Theorem mpanl12 714

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 712	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 702	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  spcimgfi1  3516  reuun1  4282  frminex  5642  tz6.26i  6351  wfii  6353  tfr2ALT  8389  tfr3ALT  8390  opthreg  9588  unsnen  10538  axcnre  11150  addgt0  11701  addgegt0  11702  addgtge0  11703  addge0  11704  addgt0i  11754  addge0i  11755  addgegt0i  11756  add20i  11758  mulge0i  11762  recextlem1  11845  recne0  11886  recdiv  11922  rec11i  11957  recgt1  12112  prodgt0i  12123  xadddi2  13324  iccshftri  13515  iccshftli  13517  iccdili  13519  icccntri  13521  mulexpz  14140  expaddz  14144  m1expeven  14147  iexpcyc  14245  cnpart  15293  resqrex  15303  sqreulem  15413  amgm2  15423  rlim  15548  ello12  15569  elo12  15580  bpolylem  16103  ege2le3  16145  dvdslelem  16368  divalglem1  16453  divalglem6  16457  divalglem9  16460  gcdaddmlem  16583  sqnprm  16762  prmlem1  17168  prmlem2  17181  m1expaddsub  19569  psgnuni  19570  gzrngunitlem  21563  lmres  23438  zdis  24955  iihalf1  25071  lmclimf  25444  vitali  25753  ismbf  25768  ismbfcn  25769  mbfconst  25773  cncombf  25798  cnmbf  25799  limcfval  26012  dvnfre  26092  quotlem  26442  ulmval  26524  ulmpm  26527  abelthlem2  26576  abelthlem3  26577  abelthlem5  26579  abelthlem7  26582  efcvx  26593  logtayl  26806  logccv  26809  cxpcn3  26894  emcllem2  27142  zetacvg  27160  basellem5  27230  bposlem7  27435  chebbnd1lem3  27616  dchrisumlem3  27636  iscgrgd  28763  axcontlem2  29296  nv1  31008  blocnilem  31137  ipasslem8  31170  siii  31186  ubthlem1  31203  norm1  31582  hhshsslem2  31601  hoscli  32095  hodcli  32096  cnlnadjlem7  32406  adjbdln  32416  pjnmopi  32481  strlem1  32583  rexdiv  33226  tpr2rico  34283  qqhre  34391  signsply0  34919  subfacval3  35662  erdszelem4  35667  erdszelem8  35671  elmrsubrn  35993  rdgprc  36265  fwddifval  36635  fwddifnval  36636  exrecfnlem  38006  poimirlem29  38281  ismblfin  38293  itg2addnclem  38303  caures  38392  sswfaxreg  45679  cjnpoly  47609  pgnbgreunbgrlem1  48861  pgnbgreunbgrlem4  48867  iooii  49679  icccldii  49680