Theorem mpanr12 701

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 699	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	mpan2 687	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 206  df-an 396

This theorem is referenced by:  wfisgOLD  6242  f1ofvswap  7158  2dom  8774  limensuci  8889  phplem4  8895  unfiOLD  9011  fiint  9021  frinsg  9440  djuen  9856  isfin1-3  10073  prlem934  10720  0idsr  10784  1idsr  10785  00sr  10786  addresr  10825  mulresr  10826  reclt1  11800  crne0  11896  nominpos  12140  expnass  13852  faclbnd2  13933  crim  14754  sqrlem1  14882  sqrlem7  14888  sqrt00  14903  sqreulem  14999  mulcn2  15233  ege2le3  15727  sin02gt0  15829  opoe  16000  oddprm  16439  pythagtriplem2  16446  pythagtriplem3  16447  pythagtriplem16  16459  pythagtrip  16463  pc1  16484  prmlem0  16735  acsfn0  17286  mgpress  19650  mgpressOLD  19651  abvneg  20009  pmatcollpw3  21841  leordtval2  22271  txswaphmeo  22864  iccntr  23890  dvlipcn  25063  sinq34lt0t  25571  cosordlem  25591  efif1olem3  25605  lgamgulmlem2  26084  basellem3  26137  ppiub  26257  bposlem9  26345  lgsne0  26388  lgsdinn0  26398  chebbnd1  26525  eupth2lem3lem4  28496  mayete3i  29991  lnop0  30229  nmcexi  30289  nmoptrii  30357  nmopcoadji  30364  hstle1  30489  hst0  30496  strlem5  30518  jplem1  30531  cnvoprabOLD  30957  subfacp1lem5  33046  limsucncmpi  34561  matunitlindflem1  35700  poimirlem15  35719  dvasin  35788  fdc  35830  eldioph3b  40503  or2expropbi  44415  ich2exprop  44811  sprsymrelfolem2  44833  sinhpcosh  46328