Theorem mp4an 709

Description: An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.)

Hypotheses

Ref	Expression
mp4an.1	|- ph
mp4an.2	|- ps
mp4an.3	|- ch
mp4an.4	|- th
mp4an.5	|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )

Assertion

Ref	Expression
mp4an	|- ta

Proof of Theorem mp4an

Step	Hyp	Ref	Expression
1		mp4an.1	. . 3 |- ph
2		mp4an.2	. . 3 |- ps
3	1, 2	pm3.2i 471	. 2 |- ( ph /\ ps )
4		mp4an.3	. . 3 |- ch
5		mp4an.4	. . 3 |- th
6	4, 5	pm3.2i 471	. 2 |- ( ch /\ th )
7		mp4an.5	. 2 |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) -> ta )
8	3, 6, 7	mp2an 708	1 |- ta

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  noinfep  8557  1lt2nq  9795  m1p1sr  9913  m1m1sr  9914  axi2m1  9980  mul4i  10233  add4i  10260  add42i  10261  addsub4i  10377  muladdi  10481  lt2addi  10590  le2addi  10591  mulne0i  10670  divne0i  10773  divmuldivi  10785  divadddivi  10787  divdivdivi  10788  subreci  10855  8th4div3  11252  xrsup0  12153  fldiv4p1lem1div2  12636  sqrt2gt1lt2  14015  3dvds2dec  15056  3dvds2decOLD  15057  flodddiv4  15137  nprmi  15402  mod2xnegi  15775  catcfuccl  16759  catcxpccl  16847  iccpnfhmeo  22744  xrhmeo  22745  cnheiborlem  22753  pcoval1  22813  pcoval2  22816  pcoass  22824  lhop1lem  23776  efcvx  24203  dvrelog  24383  dvlog  24397  dvlog2  24399  dvsqrt  24483  dvcnsqrt  24485  cxpcn3  24489  ang180lem1  24539  dvatan  24662  log2cnv  24671  log2tlbnd  24672  log2ub  24676  harmonicbnd3  24734  ppiub  24929  bposlem8  25016  bposlem9  25017  lgsdir2lem1  25050  m1lgs  25113  2lgslem4  25131  2sqlem11  25154  chebbnd1  25161  usgrexmplef  26151  siilem1  27706  hvadd4i  27915  his35i  27946  bdophsi  28955  bdopcoi  28957  mdcompli  29288  dmdcompli  29289  xrge00  29686  sqsscirc1  29954  raddcn  29975  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  esumcvgsum  30150  dstfrvclim1  30539  signsply0  30628  cvmlift2lem6  31290  cvmlift2lem12  31296  poimirlem9  33418  poimirlem15  33424  lhe4.4ex1a  38528  dvcosre  40126  wallispi  40287  fourierdlem57  40380  fourierdlem58  40381  fourierdlem112  40435  fouriersw  40448  tgblthelfgott  41703  tgblthelfgottOLD  41709  zlmodzxzequa  42285  zlmodzxzequap  42288