Theorem mpanr12 705

Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)

Hypotheses

Ref	Expression
mpanr12.1	⊢ 𝜓
mpanr12.2	⊢ 𝜒
mpanr12.3	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
mpanr12	⊢ (𝜑 → 𝜃)

Proof of Theorem mpanr12

Step	Hyp	Ref	Expression
1		mpanr12.2	. 2 ⊢ 𝜒
2		mpanr12.1	. . 3 ⊢ 𝜓
3		mpanr12.3	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	mpanr1 703	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 691	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  f1ofvswap  7252  2dom  8967  limensuci  9081  frinsg  9663  djuen  10080  isfin1-3  10296  prlem934  10944  0idsr  11008  1idsr  11009  00sr  11010  addresr  11049  mulresr  11050  reclt1  12037  crne0  12138  nominpos  12378  fvf1tp  13709  expnass  14131  faclbnd2  14214  crim  15038  01sqrexlem1  15165  01sqrexlem7  15171  sqrt00  15186  sqreulem  15283  mulcn2  15519  ege2le3  16013  sin02gt0  16117  opoe  16290  oddprm  16738  pythagtriplem2  16745  pythagtriplem3  16746  pythagtriplem16  16758  pythagtrip  16762  pc1  16783  prmlem0  17033  acsfn0  17583  mgpress  20085  abvneg  20759  pmatcollpw3  22728  leordtval2  23156  txswaphmeo  23749  iccntr  24766  dvlipcn  25955  sinq34lt0t  26474  cosordlem  26495  efif1olem3  26509  lgamgulmlem2  26996  basellem3  27049  ppiub  27171  bposlem9  27259  lgsne0  27302  lgsdinn0  27312  chebbnd1  27439  eupth2lem3lem4  30306  mayete3i  31803  lnop0  32041  nmcexi  32101  nmoptrii  32169  nmopcoadji  32176  hstle1  32301  hst0  32308  strlem5  32330  jplem1  32343  vonf1owev  35302  subfacp1lem5  35378  limsucncmpi  36639  matunitlindflem1  37817  poimirlem15  37836  dvasin  37905  fdc  37946  eldioph3b  43007  oaabsb  43536  tfsconcatfv2  43582  omssaxinf2  45229  or2expropbi  47280  ich2exprop  47717  sprsymrelfolem2  47739  clnbgrisubgrgrim  48178  sinhpcosh  49985