Theorem mp4an 694

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  noinfep  9581  1lt2nq  10896  m1p1sr  11015  m1m1sr  11016  axi2m1  11082  mul4i  11343  add4i  11371  add42i  11372  addsub4i  11490  muladdi  11601  lt2addi  11712  le2addi  11713  mulne0i  11793  divne0i  11903  divmuldivi  11915  divadddivi  11917  divdivdivi  11918  subreci  11986  8th4div3  12397  xrsup0  13275  fldiv4p1lem1div2  13794  sqrt2gt1lt2  15236  3dvds2dec  16302  flodddiv4  16384  nprmi  16658  mod2xnegi  17042  catcfuccl  18085  catcxpccl  18173  iccpnfhmeo  24912  xrhmeo  24913  cnheiborlem  24921  pcoval1  24980  pcoval2  24983  pcoass  24991  lhop1lem  25980  efcvx  26414  cos0pilt1  26496  dvrelog  26601  dvlog  26615  dvlog2  26617  dvsqrt  26706  dvcnsqrt  26708  cxpcn3  26712  ang180lem1  26773  dvatan  26899  log2cnv  26908  log2tlbnd  26909  log2ub  26913  harmonicbnd3  26971  ppiub  27167  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  m1lgs  27351  2lgslem4  27369  2sqlem11  27392  2sqreultlem  27410  2sqreunnltlem  27413  chebbnd1  27435  0lt1s  27804  twocut  28415  usgrexmplef  29328  siilem1  30922  hvadd4i  31129  his35i  31160  bdophsi  32167  bdopcoi  32169  mdcompli  32500  dmdcompli  32501  cshw1s2  33020  xrge00  33074  evl1deg3  33638  cos9thpiminplylem5  33930  sqsscirc1  34052  raddcn  34073  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  esumcvgsum  34232  dstfrvclim1  34622  signsply0  34695  cvmlift2lem6  35490  cvmlift2lem12  35496  iccioo01  37643  poimirlem9  37950  poimirlem15  37956  sqdeccom12  42721  lhe4.4ex1a  44756  dvcosre  46340  wallispi  46498  fourierdlem57  46591  fourierdlem58  46592  fourierdlem112  46646  fouriersw  46659  2exp340mod341  48209  8exp8mod9  48212  nfermltl8rev  48218  tgblthelfgott  48291  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  zlmodzxzequa  48972  zlmodzxzequap  48975  sepfsepc  49403