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  9589  1lt2nq  10902  m1p1sr  11021  m1m1sr  11022  axi2m1  11088  mul4i  11347  add4i  11375  add42i  11376  addsub4i  11494  muladdi  11605  lt2addi  11716  le2addi  11717  mulne0i  11797  divne0i  11906  divmuldivi  11918  divadddivi  11920  divdivdivi  11921  subreci  11989  8th4div3  12378  xrsup0  13259  fldiv4p1lem1div2  13773  sqrt2gt1lt2  15216  3dvds2dec  16279  flodddiv4  16361  nprmi  16635  mod2xnegi  17018  catcfuccl  18056  catcxpccl  18144  iccpnfhmeo  24819  xrhmeo  24820  cnheiborlem  24829  pcoval1  24889  pcoval2  24892  pcoass  24900  lhop1lem  25894  efcvx  26335  cos0pilt1  26417  dvrelog  26522  dvlog  26536  dvlog2  26538  dvsqrt  26627  dvcnsqrt  26629  cxpcn3  26634  ang180lem1  26695  dvatan  26821  log2cnv  26830  log2tlbnd  26831  log2ub  26835  harmonicbnd3  26894  ppiub  27091  bposlem8  27178  bposlem9  27179  lgsdir2lem1  27212  m1lgs  27275  2lgslem4  27293  2sqlem11  27316  2sqreultlem  27334  2sqreunnltlem  27337  chebbnd1  27359  0slt1s  27717  twocut  28285  usgrexmplef  29162  siilem1  30753  hvadd4i  30960  his35i  30991  bdophsi  31998  bdopcoi  32000  mdcompli  32331  dmdcompli  32332  cshw1s2  32855  xrge00  32926  evl1deg3  33520  cos9thpiminplylem5  33749  sqsscirc1  33871  raddcn  33892  xrge0iifcnv  33896  xrge0iifiso  33898  xrge0iifhom  33900  esumcvgsum  34051  dstfrvclim1  34442  signsply0  34515  cvmlift2lem6  35268  cvmlift2lem12  35274  iccioo01  37288  poimirlem9  37596  poimirlem15  37602  sqdeccom12  42250  lhe4.4ex1a  44291  dvcosre  45883  wallispi  46041  fourierdlem57  46134  fourierdlem58  46135  fourierdlem112  46189  fouriersw  46202  2exp340mod341  47707  8exp8mod9  47710  nfermltl8rev  47716  tgblthelfgott  47789  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  zlmodzxzequa  48458  zlmodzxzequap  48461  sepfsepc  48889