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  9569  1lt2nq  10884  m1p1sr  11003  m1m1sr  11004  axi2m1  11070  mul4i  11330  add4i  11358  add42i  11359  addsub4i  11477  muladdi  11588  lt2addi  11699  le2addi  11700  mulne0i  11780  divne0i  11889  divmuldivi  11901  divadddivi  11903  divdivdivi  11904  subreci  11972  8th4div3  12361  xrsup0  13238  fldiv4p1lem1div2  13755  sqrt2gt1lt2  15197  3dvds2dec  16260  flodddiv4  16342  nprmi  16616  mod2xnegi  16999  catcfuccl  18042  catcxpccl  18130  iccpnfhmeo  24899  xrhmeo  24900  cnheiborlem  24909  pcoval1  24969  pcoval2  24972  pcoass  24980  lhop1lem  25974  efcvx  26415  cos0pilt1  26497  dvrelog  26602  dvlog  26616  dvlog2  26618  dvsqrt  26707  dvcnsqrt  26709  cxpcn3  26714  ang180lem1  26775  dvatan  26901  log2cnv  26910  log2tlbnd  26911  log2ub  26915  harmonicbnd3  26974  ppiub  27171  bposlem8  27258  bposlem9  27259  lgsdir2lem1  27292  m1lgs  27355  2lgslem4  27373  2sqlem11  27396  2sqreultlem  27414  2sqreunnltlem  27417  chebbnd1  27439  0lt1s  27808  twocut  28419  usgrexmplef  29332  siilem1  30926  hvadd4i  31133  his35i  31164  bdophsi  32171  bdopcoi  32173  mdcompli  32504  dmdcompli  32505  cshw1s2  33042  xrge00  33096  evl1deg3  33659  cos9thpiminplylem5  33943  sqsscirc1  34065  raddcn  34086  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  esumcvgsum  34245  dstfrvclim1  34635  signsply0  34708  cvmlift2lem6  35502  cvmlift2lem12  35508  iccioo01  37532  poimirlem9  37830  poimirlem15  37836  sqdeccom12  42544  lhe4.4ex1a  44570  dvcosre  46156  wallispi  46314  fourierdlem57  46407  fourierdlem58  46408  fourierdlem112  46462  fouriersw  46475  2exp340mod341  47979  8exp8mod9  47982  nfermltl8rev  47988  tgblthelfgott  48061  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  zlmodzxzequa  48742  zlmodzxzequap  48745  sepfsepc  49173