Theorem mpanl12 702

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

Hypotheses

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

Assertion

Ref	Expression
mpanl12	⊢ (𝜒 → 𝜃)

Proof of Theorem mpanl12

Step	Hyp	Ref	Expression
1		mpanl12.2	. 2 ⊢ 𝜓
2		mpanl12.1	. . 3 ⊢ 𝜑
3		mpanl12.3	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	mpanl1 700	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 690	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:  reuun1  4303  frminex  5633  tz6.26i  6338  wfii  6341  wfr3OLD  8350  tfr2ALT  8413  tfr3ALT  8414  opthreg  9630  unsnen  10565  axcnre  11176  addgt0  11721  addgegt0  11722  addgtge0  11723  addge0  11724  addgt0i  11774  addge0i  11775  addgegt0i  11776  add20i  11778  mulge0i  11782  recextlem1  11865  recne0  11907  recdiv  11945  rec11i  11980  recgt1  12136  prodgt0i  12147  xadddi2  13311  iccshftri  13502  iccshftli  13504  iccdili  13506  icccntri  13508  mulexpz  14118  expaddz  14122  m1expeven  14125  iexpcyc  14223  cnpart  15257  resqrex  15267  sqreulem  15376  amgm2  15386  rlim  15509  ello12  15530  elo12  15541  bpolylem  16062  ege2le3  16104  dvdslelem  16326  divalglem1  16411  divalglem6  16415  divalglem9  16418  gcdaddmlem  16541  sqnprm  16719  prmlem1  17125  prmlem2  17137  m1expaddsub  19477  psgnuni  19478  gzrngunitlem  21398  lmres  23236  zdis  24754  iihalf1  24874  lmclimf  25254  vitali  25564  ismbf  25579  ismbfcn  25580  mbfconst  25584  cncombf  25609  cnmbf  25610  limcfval  25823  dvnfre  25906  quotlem  26258  ulmval  26339  ulmpm  26342  abelthlem2  26392  abelthlem3  26393  abelthlem5  26395  abelthlem7  26398  efcvx  26409  logtayl  26619  logccv  26622  cxpcn3  26708  emcllem2  26957  zetacvg  26975  basellem5  27045  bposlem7  27251  chebbnd1lem3  27432  dchrisumlem3  27452  iscgrgd  28438  axcontlem2  28890  nv1  30602  blocnilem  30731  ipasslem8  30764  siii  30780  ubthlem1  30797  norm1  31176  hhshsslem2  31195  hoscli  31689  hodcli  31690  cnlnadjlem7  32000  adjbdln  32010  pjnmopi  32075  strlem1  32177  rexdiv  32846  tpr2rico  33889  qqhre  33997  signsply0  34529  subfacval3  35157  erdszelem4  35162  erdszelem8  35166  elmrsubrn  35488  rdgprc  35758  fwddifval  36126  fwddifnval  36127  exrecfnlem  37343  poimirlem29  37619  ismblfin  37631  itg2addnclem  37641  caures  37730  sswfaxreg  44960  iooii  48840  icccldii  48841