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  9613  1lt2nq  10926  m1p1sr  11045  m1m1sr  11046  axi2m1  11112  mul4i  11371  add4i  11399  add42i  11400  addsub4i  11518  muladdi  11629  lt2addi  11740  le2addi  11741  mulne0i  11821  divne0i  11930  divmuldivi  11942  divadddivi  11944  divdivdivi  11945  subreci  12013  8th4div3  12402  xrsup0  13283  fldiv4p1lem1div2  13797  sqrt2gt1lt2  15240  3dvds2dec  16303  flodddiv4  16385  nprmi  16659  mod2xnegi  17042  catcfuccl  18080  catcxpccl  18168  iccpnfhmeo  24843  xrhmeo  24844  cnheiborlem  24853  pcoval1  24913  pcoval2  24916  pcoass  24924  lhop1lem  25918  efcvx  26359  cos0pilt1  26441  dvrelog  26546  dvlog  26560  dvlog2  26562  dvsqrt  26651  dvcnsqrt  26653  cxpcn3  26658  ang180lem1  26719  dvatan  26845  log2cnv  26854  log2tlbnd  26855  log2ub  26859  harmonicbnd3  26918  ppiub  27115  bposlem8  27202  bposlem9  27203  lgsdir2lem1  27236  m1lgs  27299  2lgslem4  27317  2sqlem11  27340  2sqreultlem  27358  2sqreunnltlem  27361  chebbnd1  27383  0slt1s  27741  twocut  28309  usgrexmplef  29186  siilem1  30780  hvadd4i  30987  his35i  31018  bdophsi  32025  bdopcoi  32027  mdcompli  32358  dmdcompli  32359  cshw1s2  32882  xrge00  32953  evl1deg3  33547  cos9thpiminplylem5  33776  sqsscirc1  33898  raddcn  33919  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  esumcvgsum  34078  dstfrvclim1  34469  signsply0  34542  cvmlift2lem6  35295  cvmlift2lem12  35301  iccioo01  37315  poimirlem9  37623  poimirlem15  37629  sqdeccom12  42277  lhe4.4ex1a  44318  dvcosre  45910  wallispi  46068  fourierdlem57  46161  fourierdlem58  46162  fourierdlem112  46216  fouriersw  46229  2exp340mod341  47734  8exp8mod9  47737  nfermltl8rev  47743  tgblthelfgott  47816  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  zlmodzxzequa  48485  zlmodzxzequap  48488  sepfsepc  48916