Theorem mp4an 706

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

Hypotheses

Ref	Expression
mp4an.1	⊢ 𝜑
mp4an.2	⊢ 𝜓
mp4an.3	⊢ 𝜒
mp4an.4	⊢ 𝜃
mp4an.5	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Assertion

Ref	Expression
mp4an	⊢ 𝜏

Proof of Theorem mp4an

Step	Hyp	Ref	Expression
1		mp4an.1	. . 3 ⊢ 𝜑
2		mp4an.2	. . 3 ⊢ 𝜓
3	1, 2	pm3.2i 476	. 2 ⊢ (𝜑 ∧ 𝜓)
4		mp4an.3	. . 3 ⊢ 𝜒
5		mp4an.4	. . 3 ⊢ 𝜃
6	4, 5	pm3.2i 476	. 2 ⊢ (𝜒 ∧ 𝜃)
7		mp4an.5	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
8	3, 6, 7	mp2an 705	1 ⊢ 𝜏

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  noinfep  9698  1lt2nq  11097  m1p1sr  11216  m1m1sr  11217  axi2m1  11283  mul4i  11546  add4i  11574  add42i  11575  addsub4i  11693  muladdi  11806  lt2addi  11918  le2addi  11919  mulne0i  11999  divne0i  12105  divmuldivi  12117  divadddivi  12119  divdivdivi  12120  subreci  12188  8th4div3  12606  xrsup0  13493  fldiv4p1lem1div2  14015  sqrt2gt1lt2  15484  3dvds2dec  16547  flodddiv4  16629  nprmi  16908  mod2xnegi  17293  catcfuccl  18343  catcxpccl  18431  degenmgmopdm  19184  iccpnfhmeo  25321  xrhmeo  25322  cnheiborlem  25330  pcoval1  25389  pcoval2  25392  pcoass  25400  lhop1lem  26388  efcvx  26833  cos0pilt1  26917  dvrelog  27022  dvlog  27036  dvlog2  27038  dvsqrt  27127  dvcnsqrt  27129  cxpcn3  27133  ang180lem1  27194  dvatan  27320  log2cnv  27329  log2tlbnd  27330  log2ub  27334  harmonicbnd3  27392  ppiub  27588  bposlem8  27675  bposlem9  27676  lgsdir2lem1  27709  m1lgs  27772  2lgslem4  27790  2sqlem11  27813  2sqreultlem  27831  2sqreunnltlem  27834  chebbnd1  27856  0lt1s  28255  twocut  28866  usgrexmplef  29897  siilem1  31510  hvadd4i  31717  his35i  31748  bdophsi  32755  bdopcoi  32757  mdcompli  33088  dmdcompli  33089  cshw1s2  33617  xrge00  33674  evl1deg3  34213  cos9thpiminplylem5  34529  sqsscirc1  34651  raddcn  34672  xrge0iifcnv  34676  xrge0iifiso  34678  xrge0iifhom  34680  esumcvgsum  34831  dstfrvclim1  35221  signsply0  35291  cvmlift2lem6  36281  cvmlift2lem12  36287  iccioo01  38518  poimirlem9  38815  poimirlem15  38821  sqdeccom12  43612  lhe4.4ex1a  45574  dvcosre  47195  wallispi  47353  fourierdlem57  47446  fourierdlem58  47447  fourierdlem112  47501  fouriersw  47514  2exp340mod341  49104  8exp8mod9  49107  nfermltl8rev  49113  tgblthelfgott  49186  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  zlmodzxzequa  49939  zlmodzxzequap  49942  sepfsepc  50373