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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  noinfep  9253  1lt2nq  10552  m1p1sr  10671  m1m1sr  10672  axi2m1  10738  mul4i  10994  add4i  11021  add42i  11022  addsub4i  11139  muladdi  11248  lt2addi  11359  le2addi  11360  mulne0i  11440  divne0i  11545  divmuldivi  11557  divadddivi  11559  divdivdivi  11560  subreci  11627  8th4div3  12015  xrsup0  12878  fldiv4p1lem1div2  13375  sqrt2gt1lt2  14803  3dvds2dec  15857  flodddiv4  15937  nprmi  16209  mod2xnegi  16587  catcfuccl  17579  catcfucclOLD  17580  catcxpccl  17668  catcxpcclOLD  17669  iccpnfhmeo  23796  xrhmeo  23797  cnheiborlem  23805  pcoval1  23864  pcoval2  23867  pcoass  23875  lhop1lem  24864  efcvx  25295  cos0pilt1  25375  dvrelog  25479  dvlog  25493  dvlog2  25495  dvsqrt  25582  dvcnsqrt  25584  cxpcn3  25588  ang180lem1  25646  dvatan  25772  log2cnv  25781  log2tlbnd  25782  log2ub  25786  harmonicbnd3  25844  ppiub  26039  bposlem8  26126  bposlem9  26127  lgsdir2lem1  26160  m1lgs  26223  2lgslem4  26241  2sqlem11  26264  2sqreultlem  26282  2sqreunnltlem  26285  chebbnd1  26307  usgrexmplef  27301  siilem1  28886  hvadd4i  29093  his35i  29124  bdophsi  30131  bdopcoi  30133  mdcompli  30464  dmdcompli  30465  cshw1s2  30906  xrge00  30968  sqsscirc1  31526  raddcn  31547  xrge0iifcnv  31551  xrge0iifiso  31553  xrge0iifhom  31555  esumcvgsum  31722  dstfrvclim1  32110  signsply0  32196  cvmlift2lem6  32937  cvmlift2lem12  32943  0slt1s  33709  iccioo01  35181  poimirlem9  35472  poimirlem15  35478  sqdeccom12  39965  lhe4.4ex1a  41561  dvcosre  43071  wallispi  43229  fourierdlem57  43322  fourierdlem58  43323  fourierdlem112  43377  fouriersw  43390  2exp340mod341  44801  8exp8mod9  44804  nfermltl8rev  44810  tgblthelfgott  44883  zlmodzxzequa  45453  zlmodzxzequap  45456  sepfsepc  45837