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  9625  1lt2nq  10954  m1p1sr  11073  m1m1sr  11074  axi2m1  11140  mul4i  11403  add4i  11431  add42i  11432  addsub4i  11550  muladdi  11661  lt2addi  11772  le2addi  11773  mulne0i  11853  divne0i  11959  divmuldivi  11971  divadddivi  11973  divdivdivi  11974  subreci  12042  8th4div3  12460  xrsup0  13345  fldiv4p1lem1div2  13864  sqrt2gt1lt2  15321  3dvds2dec  16387  flodddiv4  16469  nprmi  16743  mod2xnegi  17127  catcfuccl  18171  catcxpccl  18259  iccpnfhmeo  25069  xrhmeo  25070  cnheiborlem  25078  pcoval1  25137  pcoval2  25140  pcoass  25148  lhop1lem  26137  efcvx  26574  cos0pilt1  26659  dvrelog  26764  dvlog  26778  dvlog2  26780  dvsqrt  26869  dvcnsqrt  26871  cxpcn3  26875  ang180lem1  26936  dvatan  27062  log2cnv  27071  log2tlbnd  27072  log2ub  27076  harmonicbnd3  27134  ppiub  27330  bposlem8  27417  bposlem9  27418  lgsdir2lem1  27451  m1lgs  27514  2lgslem4  27532  2sqlem11  27555  2sqreultlem  27573  2sqreunnltlem  27576  chebbnd1  27598  0lt1s  27967  twocut  28578  usgrexmplef  29546  siilem1  31140  hvadd4i  31347  his35i  31378  bdophsi  32385  bdopcoi  32387  mdcompli  32718  dmdcompli  32719  cshw1s2  33217  xrge00  33271  evl1deg3  33809  cos9thpiminplylem5  34117  sqsscirc1  34239  raddcn  34260  xrge0iifcnv  34264  xrge0iifiso  34266  xrge0iifhom  34268  esumcvgsum  34419  dstfrvclim1  34809  signsply0  34879  cvmlift2lem6  35695  cvmlift2lem12  35701  iccioo01  37856  poimirlem9  38163  poimirlem15  38169  sqdeccom12  42933  lhe4.4ex1a  44924  dvcosre  46511  wallispi  46669  fourierdlem57  46762  fourierdlem58  46763  fourierdlem112  46817  fouriersw  46830  2exp340mod341  48380  8exp8mod9  48383  nfermltl8rev  48389  tgblthelfgott  48462  pgnbgreunbgrlem2lem1  48761  pgnbgreunbgrlem2lem2  48762  pgnbgreunbgrlem2lem3  48763  zlmodzxzequa  49154  zlmodzxzequap  49157  sepfsepc  49584