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  7281  2dom  9001  limensuci  9117  fiintOLD  9278  frinsg  9704  djuen  10123  isfin1-3  10339  prlem934  10986  0idsr  11050  1idsr  11051  00sr  11052  addresr  11091  mulresr  11092  reclt1  12078  crne0  12179  nominpos  12419  fvf1tp  13751  expnass  14173  faclbnd2  14256  crim  15081  01sqrexlem1  15208  01sqrexlem7  15214  sqrt00  15229  sqreulem  15326  mulcn2  15562  ege2le3  16056  sin02gt0  16160  opoe  16333  oddprm  16781  pythagtriplem2  16788  pythagtriplem3  16789  pythagtriplem16  16801  pythagtrip  16805  pc1  16826  prmlem0  17076  acsfn0  17621  mgpress  20059  abvneg  20735  pmatcollpw3  22671  leordtval2  23099  txswaphmeo  23692  iccntr  24710  dvlipcn  25899  sinq34lt0t  26418  cosordlem  26439  efif1olem3  26453  lgamgulmlem2  26940  basellem3  26993  ppiub  27115  bposlem9  27203  lgsne0  27246  lgsdinn0  27256  chebbnd1  27383  eupth2lem3lem4  30160  mayete3i  31657  lnop0  31895  nmcexi  31955  nmoptrii  32023  nmopcoadji  32030  hstle1  32155  hst0  32162  strlem5  32184  jplem1  32197  vonf1owev  35095  subfacp1lem5  35171  limsucncmpi  36433  matunitlindflem1  37610  poimirlem15  37629  dvasin  37698  fdc  37739  eldioph3b  42753  oaabsb  43283  tfsconcatfv2  43329  omssaxinf2  44978  or2expropbi  47035  ich2exprop  47472  sprsymrelfolem2  47494  clnbgrisubgrgrim  47932  sinhpcosh  49729