Theorem mp4an 690

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 471	. 2 ⊢ (𝜑 ∧ 𝜓)
4		mp4an.3	. . 3 ⊢ 𝜒
5		mp4an.4	. . 3 ⊢ 𝜃
6	4, 5	pm3.2i 471	. 2 ⊢ (𝜒 ∧ 𝜃)
7		mp4an.5	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
8	3, 6, 7	mp2an 689	1 ⊢ 𝜏

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  noinfep  9427  1lt2nq  10738  m1p1sr  10857  m1m1sr  10858  axi2m1  10924  mul4i  11181  add4i  11208  add42i  11209  addsub4i  11326  muladdi  11435  lt2addi  11546  le2addi  11547  mulne0i  11627  divne0i  11732  divmuldivi  11744  divadddivi  11746  divdivdivi  11747  subreci  11814  8th4div3  12202  xrsup0  13066  fldiv4p1lem1div2  13564  sqrt2gt1lt2  14995  3dvds2dec  16051  flodddiv4  16131  nprmi  16403  mod2xnegi  16781  catcfuccl  17843  catcfucclOLD  17844  catcxpccl  17933  catcxpcclOLD  17934  iccpnfhmeo  24117  xrhmeo  24118  cnheiborlem  24126  pcoval1  24185  pcoval2  24188  pcoass  24196  lhop1lem  25186  efcvx  25617  cos0pilt1  25697  dvrelog  25801  dvlog  25815  dvlog2  25817  dvsqrt  25904  dvcnsqrt  25906  cxpcn3  25910  ang180lem1  25968  dvatan  26094  log2cnv  26103  log2tlbnd  26104  log2ub  26108  harmonicbnd3  26166  ppiub  26361  bposlem8  26448  bposlem9  26449  lgsdir2lem1  26482  m1lgs  26545  2lgslem4  26563  2sqlem11  26586  2sqreultlem  26604  2sqreunnltlem  26607  chebbnd1  26629  usgrexmplef  27635  siilem1  29222  hvadd4i  29429  his35i  29460  bdophsi  30467  bdopcoi  30469  mdcompli  30800  dmdcompli  30801  cshw1s2  31241  xrge00  31304  sqsscirc1  31867  raddcn  31888  xrge0iifcnv  31892  xrge0iifiso  31894  xrge0iifhom  31896  esumcvgsum  32065  dstfrvclim1  32453  signsply0  32539  cvmlift2lem6  33279  cvmlift2lem12  33285  0slt1s  34032  iccioo01  35507  poimirlem9  35795  poimirlem15  35801  sqdeccom12  40324  lhe4.4ex1a  41954  dvcosre  43460  wallispi  43618  fourierdlem57  43711  fourierdlem58  43712  fourierdlem112  43766  fouriersw  43779  2exp340mod341  45196  8exp8mod9  45199  nfermltl8rev  45205  tgblthelfgott  45278  zlmodzxzequa  45848  zlmodzxzequap  45851  sepfsepc  46232