Theorem mp4an 711

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  noinfep  8732  1lt2nq  10007  m1p1sr  10125  m1m1sr  10126  axi2m1  10192  mul4i  10445  add4i  10472  add42i  10473  addsub4i  10589  muladdi  10693  lt2addi  10802  le2addi  10803  mulne0i  10882  divne0i  10985  divmuldivi  10997  divadddivi  10999  divdivdivi  11000  subreci  11067  8th4div3  11464  xrsup0  12366  fldiv4p1lem1div2  12850  sqrt2gt1lt2  14234  3dvds2dec  15278  3dvds2decOLD  15279  flodddiv4  15359  nprmi  15624  mod2xnegi  15997  catcfuccl  16980  catcxpccl  17068  iccpnfhmeo  22965  xrhmeo  22966  cnheiborlem  22974  pcoval1  23033  pcoval2  23036  pcoass  23044  lhop1lem  23995  efcvx  24422  dvrelog  24603  dvlog  24617  dvlog2  24619  dvsqrt  24703  dvcnsqrt  24705  cxpcn3  24709  ang180lem1  24759  dvatan  24882  log2cnv  24891  log2tlbnd  24892  log2ub  24896  harmonicbnd3  24954  ppiub  25149  bposlem8  25236  bposlem9  25237  lgsdir2lem1  25270  m1lgs  25333  2lgslem4  25351  2sqlem11  25374  chebbnd1  25381  usgrexmplef  26371  siilem1  28036  hvadd4i  28245  his35i  28276  bdophsi  29285  bdopcoi  29287  mdcompli  29618  dmdcompli  29619  xrge00  30016  sqsscirc1  30284  raddcn  30305  xrge0iifcnv  30309  xrge0iifiso  30311  xrge0iifhom  30313  esumcvgsum  30480  dstfrvclim1  30869  signsply0  30958  cvmlift2lem6  31618  cvmlift2lem12  31624  poimirlem9  33749  poimirlem15  33755  lhe4.4ex1a  39048  dvcosre  40647  wallispi  40808  fourierdlem57  40901  fourierdlem58  40902  fourierdlem112  40956  fouriersw  40969  tgblthelfgott  42231  tgblthelfgottOLD  42237  zlmodzxzequa  42813  zlmodzxzequap  42816