Theorem mp4an 703

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  noinfep  9609  1lt2nq  10925  m1p1sr  11044  m1m1sr  11045  axi2m1  11111  mul4i  11374  add4i  11402  add42i  11403  addsub4i  11521  muladdi  11632  lt2addi  11743  le2addi  11744  mulne0i  11824  divne0i  11933  divmuldivi  11945  divadddivi  11947  divdivdivi  11948  subreci  12016  8th4div3  12435  xrsup0  13320  fldiv4p1lem1div2  13839  sqrt2gt1lt2  15292  3dvds2dec  16358  flodddiv4  16440  nprmi  16714  mod2xnegi  17098  catcfuccl  18142  catcxpccl  18230  iccpnfhmeo  24995  xrhmeo  24996  cnheiborlem  25004  pcoval1  25063  pcoval2  25066  pcoass  25074  lhop1lem  26063  efcvx  26500  cos0pilt1  26585  dvrelog  26690  dvlog  26704  dvlog2  26706  dvsqrt  26795  dvcnsqrt  26797  cxpcn3  26801  ang180lem1  26862  dvatan  26988  log2cnv  26997  log2tlbnd  26998  log2ub  27002  harmonicbnd3  27060  ppiub  27256  bposlem8  27343  bposlem9  27344  lgsdir2lem1  27377  m1lgs  27440  2lgslem4  27458  2sqlem11  27481  2sqreultlem  27499  2sqreunnltlem  27502  chebbnd1  27524  0lt1s  27893  twocut  28504  usgrexmplef  29417  siilem1  31011  hvadd4i  31218  his35i  31249  bdophsi  32256  bdopcoi  32258  mdcompli  32589  dmdcompli  32590  cshw1s2  33099  xrge00  33153  evl1deg3  33735  cos9thpiminplylem5  34044  sqsscirc1  34166  raddcn  34187  xrge0iifcnv  34191  xrge0iifiso  34193  xrge0iifhom  34195  esumcvgsum  34346  dstfrvclim1  34736  signsply0  34806  cvmlift2lem6  35619  cvmlift2lem12  35625  iccioo01  37782  poimirlem9  38089  poimirlem15  38095  sqdeccom12  42859  lhe4.4ex1a  44866  dvcosre  46447  wallispi  46605  fourierdlem57  46698  fourierdlem58  46699  fourierdlem112  46753  fouriersw  46766  2exp340mod341  48316  8exp8mod9  48319  nfermltl8rev  48325  tgblthelfgott  48398  pgnbgreunbgrlem2lem1  48697  pgnbgreunbgrlem2lem2  48698  pgnbgreunbgrlem2lem3  48699  zlmodzxzequa  49079  zlmodzxzequap  49082  sepfsepc  49510