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  9117  1lt2nq  10389  m1p1sr  10508  m1m1sr  10509  axi2m1  10575  mul4i  10831  add4i  10858  add42i  10859  addsub4i  10976  muladdi  11085  lt2addi  11196  le2addi  11197  mulne0i  11277  divne0i  11382  divmuldivi  11394  divadddivi  11396  divdivdivi  11397  subreci  11464  8th4div3  11851  xrsup0  12710  fldiv4p1lem1div2  13199  sqrt2gt1lt2  14628  3dvds2dec  15676  flodddiv4  15758  nprmi  16027  mod2xnegi  16401  catcfuccl  17363  catcxpccl  17451  iccpnfhmeo  23543  xrhmeo  23544  cnheiborlem  23552  pcoval1  23611  pcoval2  23614  pcoass  23622  lhop1lem  24604  efcvx  25031  dvrelog  25214  dvlog  25228  dvlog2  25230  dvsqrt  25317  dvcnsqrt  25319  cxpcn3  25323  ang180lem1  25381  dvatan  25507  log2cnv  25516  log2tlbnd  25517  log2ub  25521  harmonicbnd3  25579  ppiub  25774  bposlem8  25861  bposlem9  25862  lgsdir2lem1  25895  m1lgs  25958  2lgslem4  25976  2sqlem11  25999  2sqreultlem  26017  2sqreunnltlem  26020  chebbnd1  26042  usgrexmplef  27035  siilem1  28622  hvadd4i  28829  his35i  28860  bdophsi  29867  bdopcoi  29869  mdcompli  30200  dmdcompli  30201  cshw1s2  30629  xrge00  30668  sqsscirc1  31146  raddcn  31167  xrge0iifcnv  31171  xrge0iifiso  31173  xrge0iifhom  31175  esumcvgsum  31342  dstfrvclim1  31730  signsply0  31816  cvmlift2lem6  32550  cvmlift2lem12  32556  poimirlem9  34895  poimirlem15  34901  sqdeccom12  39168  lhe4.4ex1a  40654  dvcosre  42189  wallispi  42349  fourierdlem57  42442  fourierdlem58  42443  fourierdlem112  42497  fouriersw  42510  2exp340mod341  43892  8exp8mod9  43895  nfermltl8rev  43901  tgblthelfgott  43974  zlmodzxzequa  44545  zlmodzxzequap  44548