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  9665  1lt2nq  11062  m1p1sr  11181  m1m1sr  11182  axi2m1  11248  mul4i  11511  add4i  11539  add42i  11540  addsub4i  11658  muladdi  11771  lt2addi  11882  le2addi  11883  mulne0i  11963  divne0i  12069  divmuldivi  12081  divadddivi  12083  divdivdivi  12084  subreci  12152  8th4div3  12570  xrsup0  13457  fldiv4p1lem1div2  13979  sqrt2gt1lt2  15447  3dvds2dec  16509  flodddiv4  16591  nprmi  16870  mod2xnegi  17255  catcfuccl  18299  catcxpccl  18387  degenmgmopdm  19140  iccpnfhmeo  25272  xrhmeo  25273  cnheiborlem  25281  pcoval1  25340  pcoval2  25343  pcoass  25351  lhop1lem  26339  efcvx  26782  cos0pilt1  26866  dvrelog  26971  dvlog  26985  dvlog2  26987  dvsqrt  27076  dvcnsqrt  27078  cxpcn3  27082  ang180lem1  27143  dvatan  27269  log2cnv  27278  log2tlbnd  27279  log2ub  27283  harmonicbnd3  27341  ppiub  27537  bposlem8  27624  bposlem9  27625  lgsdir2lem1  27658  m1lgs  27721  2lgslem4  27739  2sqlem11  27762  2sqreultlem  27780  2sqreunnltlem  27783  chebbnd1  27805  0lt1s  28204  twocut  28815  usgrexmplef  29846  siilem1  31459  hvadd4i  31666  his35i  31697  bdophsi  32704  bdopcoi  32706  mdcompli  33037  dmdcompli  33038  cshw1s2  33568  xrge00  33622  evl1deg3  34157  cos9thpiminplylem5  34465  sqsscirc1  34587  raddcn  34608  xrge0iifcnv  34612  xrge0iifiso  34614  xrge0iifhom  34616  esumcvgsum  34767  dstfrvclim1  35157  signsply0  35227  cvmlift2lem6  36160  cvmlift2lem12  36166  iccioo01  38344  poimirlem9  38641  poimirlem15  38647  sqdeccom12  43440  lhe4.4ex1a  45407  dvcosre  47016  wallispi  47174  fourierdlem57  47267  fourierdlem58  47268  fourierdlem112  47322  fouriersw  47335  2exp340mod341  48925  8exp8mod9  48928  nfermltl8rev  48934  tgblthelfgott  49007  pgnbgreunbgrlem2lem1  49306  pgnbgreunbgrlem2lem2  49307  pgnbgreunbgrlem2lem3  49308  zlmodzxzequa  49702  zlmodzxzequap  49705  sepfsepc  50136