Theorem mp4an 705

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 704	1 ⊢ 𝜏

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  noinfep  8440  1lt2nq  9674  m1p1sr  9792  m1m1sr  9793  axi2m1  9859  mul4i  10112  add4i  10139  add42i  10140  addsub4i  10256  muladdi  10360  lt2addi  10469  le2addi  10470  mulne0i  10549  divne0i  10652  divmuldivi  10664  divadddivi  10666  divdivdivi  10667  subreci  10734  8th4div3  11129  xrsup0  12025  fldiv4p1lem1div2  12498  sqrt2gt1lt2  13863  3dvds2dec  14894  3dvds2decOLD  14895  flodddiv4  14975  nprmi  15240  mod2xnegi  15613  catcfuccl  16582  catcxpccl  16670  iccpnfhmeo  22552  xrhmeo  22553  cnheiborlem  22561  pcoval1  22621  pcoval2  22624  pcoass  22632  lhop1lem  23580  efcvx  24007  dvrelog  24183  dvlog  24197  dvlog2  24199  dvsqrt  24283  dvcnsqrt  24285  cxpcn3  24289  ang180lem1  24339  dvatan  24462  log2cnv  24471  log2tlbnd  24472  log2ub  24476  harmonicbnd3  24534  ppiub  24729  bposlem8  24816  bposlem9  24817  lgsdir2lem1  24850  m1lgs  24913  2lgslem4  24931  2sqlem11  24954  chebbnd1  24961  usgraexmplef  25929  constr3lem4  26175  vdegp1ai  26511  vdegp1bi  26512  siilem1  27090  hvadd4i  27299  his35i  27330  bdophsi  28339  bdopcoi  28341  mdcompli  28672  dmdcompli  28673  xrge00  29017  sqsscirc1  29282  raddcn  29303  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  esumcvgsum  29477  dstfrvclim1  29866  signsply0  29954  cvmlift2lem6  30544  cvmlift2lem12  30550  poimirlem9  32588  poimirlem15  32594  lhe4.4ex1a  37550  dvcosre  38799  wallispi  38963  fourierdlem57  39056  fourierdlem58  39057  fourierdlem112  39111  fouriersw  39124  tgblthelfgott  40229  tgblthelfgottOLD  40236  zlmodzxzequa  42079  zlmodzxzequap  42082