Theorem mp4an 693

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 692	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  9679  1lt2nq  10992  m1p1sr  11111  m1m1sr  11112  axi2m1  11178  mul4i  11437  add4i  11465  add42i  11466  addsub4i  11584  muladdi  11693  lt2addi  11804  le2addi  11805  mulne0i  11885  divne0i  11994  divmuldivi  12006  divadddivi  12008  divdivdivi  12009  subreci  12077  8th4div3  12466  xrsup0  13344  fldiv4p1lem1div2  13857  sqrt2gt1lt2  15298  3dvds2dec  16357  flodddiv4  16439  nprmi  16713  mod2xnegi  17096  catcfuccl  18136  catcxpccl  18224  iccpnfhmeo  24899  xrhmeo  24900  cnheiborlem  24909  pcoval1  24969  pcoval2  24972  pcoass  24980  lhop1lem  25975  efcvx  26416  cos0pilt1  26498  dvrelog  26603  dvlog  26617  dvlog2  26619  dvsqrt  26708  dvcnsqrt  26710  cxpcn3  26715  ang180lem1  26776  dvatan  26902  log2cnv  26911  log2tlbnd  26912  log2ub  26916  harmonicbnd3  26975  ppiub  27172  bposlem8  27259  bposlem9  27260  lgsdir2lem1  27293  m1lgs  27356  2lgslem4  27374  2sqlem11  27397  2sqreultlem  27415  2sqreunnltlem  27418  chebbnd1  27440  0slt1s  27798  twocut  28366  usgrexmplef  29243  siilem1  30837  hvadd4i  31044  his35i  31075  bdophsi  32082  bdopcoi  32084  mdcompli  32415  dmdcompli  32416  cshw1s2  32941  xrge00  33012  evl1deg3  33596  cos9thpiminplylem5  33825  sqsscirc1  33944  raddcn  33965  xrge0iifcnv  33969  xrge0iifiso  33971  xrge0iifhom  33973  esumcvgsum  34124  dstfrvclim1  34515  signsply0  34588  cvmlift2lem6  35335  cvmlift2lem12  35341  iccioo01  37350  poimirlem9  37658  poimirlem15  37664  sqdeccom12  42307  lhe4.4ex1a  44328  dvcosre  45921  wallispi  46079  fourierdlem57  46172  fourierdlem58  46173  fourierdlem112  46227  fouriersw  46240  2exp340mod341  47727  8exp8mod9  47730  nfermltl8rev  47736  tgblthelfgott  47809  zlmodzxzequa  48452  zlmodzxzequap  48455  sepfsepc  48882