Theorem mp4an 705

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  noinfep  9630  1lt2nq  10959  m1p1sr  11078  m1m1sr  11079  axi2m1  11145  mul4i  11408  add4i  11436  add42i  11437  addsub4i  11555  muladdi  11666  lt2addi  11777  le2addi  11778  mulne0i  11858  divne0i  11964  divmuldivi  11976  divadddivi  11978  divdivdivi  11979  subreci  12047  8th4div3  12465  xrsup0  13350  fldiv4p1lem1div2  13870  sqrt2gt1lt2  15327  3dvds2dec  16392  flodddiv4  16474  nprmi  16748  mod2xnegi  17132  catcfuccl  18176  catcxpccl  18264  iccpnfhmeo  25085  xrhmeo  25086  cnheiborlem  25094  pcoval1  25153  pcoval2  25156  pcoass  25164  lhop1lem  26153  efcvx  26593  cos0pilt1  26678  dvrelog  26783  dvlog  26797  dvlog2  26799  dvsqrt  26888  dvcnsqrt  26890  cxpcn3  26894  ang180lem1  26955  dvatan  27081  log2cnv  27090  log2tlbnd  27091  log2ub  27095  harmonicbnd3  27153  ppiub  27349  bposlem8  27436  bposlem9  27437  lgsdir2lem1  27470  m1lgs  27533  2lgslem4  27551  2sqlem11  27574  2sqreultlem  27592  2sqreunnltlem  27595  chebbnd1  27617  0lt1s  27986  twocut  28597  usgrexmplef  29590  siilem1  31184  hvadd4i  31391  his35i  31422  bdophsi  32429  bdopcoi  32431  mdcompli  32762  dmdcompli  32763  cshw1s2  33261  xrge00  33315  evl1deg3  33849  cos9thpiminplylem5  34157  sqsscirc1  34279  raddcn  34300  xrge0iifcnv  34304  xrge0iifiso  34306  xrge0iifhom  34308  esumcvgsum  34459  dstfrvclim1  34849  signsply0  34919  cvmlift2lem6  35781  cvmlift2lem12  35787  iccioo01  37954  poimirlem9  38261  poimirlem15  38267  sqdeccom12  43031  lhe4.4ex1a  45022  dvcosre  46609  wallispi  46767  fourierdlem57  46860  fourierdlem58  46861  fourierdlem112  46915  fouriersw  46928  2exp340mod341  48481  8exp8mod9  48484  nfermltl8rev  48490  tgblthelfgott  48563  pgnbgreunbgrlem2lem1  48862  pgnbgreunbgrlem2lem2  48863  pgnbgreunbgrlem2lem3  48864  zlmodzxzequa  49259  zlmodzxzequap  49262  sepfsepc  49689