Theorem mpanr12 703

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 701	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 689	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  wfisg  6176  2dom  8574  limensuci  8685  phplem4  8691  unfi  8777  fiint  8787  djuen  9587  isfin1-3  9800  prlem934  10447  0idsr  10511  1idsr  10512  00sr  10513  addresr  10552  mulresr  10553  reclt1  11527  crne0  11623  nominpos  11866  expnass  13562  faclbnd2  13643  crim  14466  sqrlem1  14594  sqrlem7  14600  sqrt00  14615  sqreulem  14711  mulcn2  14944  ege2le3  15435  sin02gt0  15537  opoe  15704  oddprm  16139  pythagtriplem2  16146  pythagtriplem3  16147  pythagtriplem16  16159  pythagtrip  16163  pc1  16184  prmlem0  16431  acsfn0  16923  mgpress  19242  abvneg  19597  pmatcollpw3  21384  leordtval2  21812  txswaphmeo  22405  iccntr  23421  dvlipcn  24583  sinq34lt0t  25087  cosordlem  25107  efif1olem3  25120  lgamgulmlem2  25599  basellem3  25652  ppiub  25772  bposlem9  25860  lgsne0  25903  lgsdinn0  25913  chebbnd1  26040  eupth2lem3lem4  28002  mayete3i  29497  lnop0  29735  nmcexi  29795  nmoptrii  29863  nmopcoadji  29870  hstle1  29995  hst0  30002  strlem5  30024  jplem1  30037  cnvoprabOLD  30448  subfacp1lem5  32424  frinsg  33080  limsucncmpi  33786  matunitlindflem1  34880  poimirlem15  34899  dvasin  34970  fdc  35012  eldioph3b  39352  or2expropbi  43259  ich2exprop  43623  sprsymrelfolem2  43645  sinhpcosh  44829