Theorem mpanr12 706

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 704	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 692	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  7254  2dom  8970  limensuci  9084  frinsg  9666  djuen  10083  isfin1-3  10299  prlem934  10947  0idsr  11011  1idsr  11012  00sr  11013  addresr  11052  mulresr  11053  reclt1  12042  crne0  12143  nominpos  12405  fvf1tp  13739  expnass  14161  faclbnd2  14244  crim  15068  01sqrexlem1  15195  01sqrexlem7  15201  sqrt00  15216  sqreulem  15313  mulcn2  15549  ege2le3  16046  sin02gt0  16150  opoe  16323  oddprm  16772  pythagtriplem2  16779  pythagtriplem3  16780  pythagtriplem16  16792  pythagtrip  16796  pc1  16817  prmlem0  17067  acsfn0  17617  mgpress  20122  abvneg  20794  pmatcollpw3  22759  leordtval2  23187  txswaphmeo  23780  iccntr  24797  dvlipcn  25971  sinq34lt0t  26486  cosordlem  26507  efif1olem3  26521  lgamgulmlem2  27007  basellem3  27060  ppiub  27181  bposlem9  27269  lgsne0  27312  lgsdinn0  27322  chebbnd1  27449  eupth2lem3lem4  30316  mayete3i  31814  lnop0  32052  nmcexi  32112  nmoptrii  32180  nmopcoadji  32187  hstle1  32312  hst0  32319  strlem5  32341  jplem1  32354  vonf1owev  35306  subfacp1lem5  35382  limsucncmpi  36643  matunitlindflem1  37951  poimirlem15  37970  dvasin  38039  fdc  38080  eldioph3b  43211  oaabsb  43740  tfsconcatfv2  43786  omssaxinf2  45433  or2expropbi  47494  ich2exprop  47943  sprsymrelfolem2  47965  clnbgrisubgrgrim  48420  sinhpcosh  50227