Theorem mp4an 691

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  noinfep  9126  1lt2nq  10398  m1p1sr  10517  m1m1sr  10518  axi2m1  10584  mul4i  10840  add4i  10867  add42i  10868  addsub4i  10985  muladdi  11094  lt2addi  11205  le2addi  11206  mulne0i  11286  divne0i  11391  divmuldivi  11403  divadddivi  11405  divdivdivi  11406  subreci  11473  8th4div3  11860  xrsup0  12719  fldiv4p1lem1div2  13208  sqrt2gt1lt2  14637  3dvds2dec  15685  flodddiv4  15767  nprmi  16036  mod2xnegi  16410  catcfuccl  17372  catcxpccl  17460  iccpnfhmeo  23552  xrhmeo  23553  cnheiborlem  23561  pcoval1  23620  pcoval2  23623  pcoass  23631  lhop1lem  24613  efcvx  25040  dvrelog  25223  dvlog  25237  dvlog2  25239  dvsqrt  25326  dvcnsqrt  25328  cxpcn3  25332  ang180lem1  25390  dvatan  25516  log2cnv  25525  log2tlbnd  25526  log2ub  25530  harmonicbnd3  25588  ppiub  25783  bposlem8  25870  bposlem9  25871  lgsdir2lem1  25904  m1lgs  25967  2lgslem4  25985  2sqlem11  26008  2sqreultlem  26026  2sqreunnltlem  26029  chebbnd1  26051  usgrexmplef  27044  siilem1  28631  hvadd4i  28838  his35i  28869  bdophsi  29876  bdopcoi  29878  mdcompli  30209  dmdcompli  30210  cshw1s2  30638  xrge00  30677  sqsscirc1  31155  raddcn  31176  xrge0iifcnv  31180  xrge0iifiso  31182  xrge0iifhom  31184  esumcvgsum  31351  dstfrvclim1  31739  signsply0  31825  cvmlift2lem6  32559  cvmlift2lem12  32565  poimirlem9  34905  poimirlem15  34911  sqdeccom12  39181  lhe4.4ex1a  40667  dvcosre  42202  wallispi  42362  fourierdlem57  42455  fourierdlem58  42456  fourierdlem112  42510  fouriersw  42523  2exp340mod341  43905  8exp8mod9  43908  nfermltl8rev  43914  tgblthelfgott  43987  zlmodzxzequa  44558  zlmodzxzequap  44561