Theorem mp4an 704

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 469	. 2 ⊢ (𝜑 ∧ 𝜓)
4		mp4an.3	. . 3 ⊢ 𝜒
5		mp4an.4	. . 3 ⊢ 𝜃
6	4, 5	pm3.2i 469	. 2 ⊢ (𝜒 ∧ 𝜃)
7		mp4an.5	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)
8	3, 6, 7	mp2an 703	1 ⊢ 𝜏

Syntax hints:   → wi 4   ∧ wa 382

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 195  df-an 384

This theorem is referenced by:  noinfep  8413  1lt2nq  9647  m1p1sr  9765  m1m1sr  9766  axi2m1  9832  mul4i  10080  add4i  10107  add42i  10108  addsub4i  10224  muladdi  10327  lt2addi  10435  le2addi  10436  mulne0i  10515  divne0i  10618  divmuldivi  10630  divadddivi  10632  divdivdivi  10633  subreci  10700  8th4div3  11095  xrsup0  11977  fldiv4p1lem1div2  12449  sqrt2gt1lt2  13805  3dvds2dec  14836  3dvds2decOLD  14837  flodddiv4  14917  nprmi  15182  mod2xnegi  15555  catcfuccl  16524  catcxpccl  16612  iccpnfhmeo  22479  xrhmeo  22480  cnheiborlem  22488  pcoval1  22548  pcoval2  22551  pcoass  22559  lhop1lem  23493  efcvx  23920  dvrelog  24096  dvlog  24110  dvlog2  24112  dvsqrt  24196  dvcnsqrt  24198  cxpcn3  24202  ang180lem1  24252  dvatan  24375  log2cnv  24384  log2tlbnd  24385  log2ub  24389  harmonicbnd3  24447  ppiub  24642  bposlem8  24729  bposlem9  24730  lgsdir2lem1  24763  m1lgs  24826  2lgslem4  24844  2sqlem11  24867  chebbnd1  24874  usgraexmplef  25691  constr3lem4  25937  vdegp1ai  26273  vdegp1bi  26274  siilem1  26892  hvadd4i  27101  his35i  27132  bdophsi  28141  bdopcoi  28143  mdcompli  28474  dmdcompli  28475  xrge00  28819  sqsscirc1  29084  raddcn  29105  xrge0iifcnv  29109  xrge0iifiso  29111  xrge0iifhom  29113  esumcvgsum  29279  dstfrvclim1  29668  signsply0  29756  cvmlift2lem6  30346  cvmlift2lem12  30352  poimirlem9  32387  poimirlem15  32393  lhe4.4ex1a  37349  dvcosre  38599  wallispi  38763  fourierdlem57  38856  fourierdlem58  38857  fourierdlem112  38911  fouriersw  38924  tgblthelfgott  40030  tgblthelfgottOLD  40037  zlmodzxzequa  42077  zlmodzxzequap  42080