Theorem mp4an 706

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  noinfep  9654  1lt2nq  11051  m1p1sr  11170  m1m1sr  11171  axi2m1  11237  mul4i  11500  add4i  11528  add42i  11529  addsub4i  11647  muladdi  11760  lt2addi  11871  le2addi  11872  mulne0i  11952  divne0i  12058  divmuldivi  12070  divadddivi  12072  divdivdivi  12073  subreci  12141  8th4div3  12559  xrsup0  13446  fldiv4p1lem1div2  13968  sqrt2gt1lt2  15434  3dvds2dec  16496  flodddiv4  16578  nprmi  16857  mod2xnegi  17242  catcfuccl  18286  catcxpccl  18374  degenmgmopdm  19127  iccpnfhmeo  25259  xrhmeo  25260  cnheiborlem  25268  pcoval1  25327  pcoval2  25330  pcoass  25338  lhop1lem  26326  efcvx  26769  cos0pilt1  26853  dvrelog  26958  dvlog  26972  dvlog2  26974  dvsqrt  27063  dvcnsqrt  27065  cxpcn3  27069  ang180lem1  27130  dvatan  27256  log2cnv  27265  log2tlbnd  27266  log2ub  27270  harmonicbnd3  27328  ppiub  27524  bposlem8  27611  bposlem9  27612  lgsdir2lem1  27645  m1lgs  27708  2lgslem4  27726  2sqlem11  27749  2sqreultlem  27767  2sqreunnltlem  27770  chebbnd1  27792  0lt1s  28191  twocut  28802  usgrexmplef  29833  siilem1  31446  hvadd4i  31653  his35i  31684  bdophsi  32691  bdopcoi  32693  mdcompli  33024  dmdcompli  33025  cshw1s2  33514  xrge00  33568  evl1deg3  34103  cos9thpiminplylem5  34411  sqsscirc1  34533  raddcn  34554  xrge0iifcnv  34558  xrge0iifiso  34560  xrge0iifhom  34562  esumcvgsum  34713  dstfrvclim1  35103  signsply0  35173  cvmlift2lem6  36052  cvmlift2lem12  36058  iccioo01  38230  poimirlem9  38527  poimirlem15  38533  sqdeccom12  43326  lhe4.4ex1a  45298  dvcosre  46891  wallispi  47049  fourierdlem57  47142  fourierdlem58  47143  fourierdlem112  47197  fouriersw  47210  2exp340mod341  48800  8exp8mod9  48803  nfermltl8rev  48809  tgblthelfgott  48882  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  pgnbgreunbgrlem2lem3  49183  zlmodzxzequa  49577  zlmodzxzequap  49580  sepfsepc  50005