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 383

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 196  df-an 385

This theorem is referenced by:  reuun1  3868  frminex  5018  tz6.26i  5629  wfii  5631  opthreg  8398  unsnen  9254  axcnre  9864  addgt0  10393  addgegt0  10394  addgtge0  10395  addge0  10396  addgt0i  10446  addge0i  10447  addgegt0i  10448  add20i  10450  mulge0i  10454  recextlem1  10536  recne0  10577  recdiv  10610  rec11i  10645  recgt1  10798  prodgt0i  10809  prodge0i  10810  xadddi2  11999  iccshftri  12178  iccshftli  12180  iccdili  12182  icccntri  12184  mulexpz  12762  expaddz  12766  m1expeven  12769  iexpcyc  12831  cnpart  13828  resqrex  13839  sqreulem  13947  amgm2  13957  rlim  14074  ello12  14095  elo12  14106  efcllem  14647  ege2le3  14659  dvdslelem  14869  divalglem1  14955  divalglem6  14959  divalglem9  14962  gcdaddmlem  15083  sqnprm  15252  prmlem1  15652  prmlem2  15665  xpscfn  16042  m1expaddsub  17741  psgnuni  17742  gzrngunitlem  19630  lmres  20914  zdis  22427  iihalf1  22538  lmclimf  22910  vitali  23188  ismbf  23203  ismbfcn  23204  mbfconst  23208  cncombf  23231  cnmbf  23232  limcfval  23442  dvnfre  23521  quotlem  23859  ulmval  23938  ulmpm  23941  abelthlem2  23990  abelthlem3  23991  abelthlem5  23993  abelthlem7  23996  efcvx  24007  logtayl  24206  logccv  24209  cxpcn3  24289  emcllem2  24523  zetacvg  24541  basellem5  24611  bposlem7  24815  chebbnd1lem3  24960  dchrisumlem3  24980  iscgrgd  25208  axcontlem2  25645  nv1  26914  blocnilem  27043  ipasslem8  27076  siii  27092  ubthlem1  27110  norm1  27490  hhshsslem2  27509  hoscli  28005  hodcli  28006  cnlnadjlem7  28316  adjbdln  28326  pjnmopi  28391  strlem1  28493  rexdiv  28965  tpr2rico  29286  qqhre  29392  signsply0  29954  subfacval3  30425  erdszelem4  30430  erdszelem8  30434  elmrsubrn  30671  rdgprc  30944  frindi  30985  fwddifval  31439  fwddifnval  31440  poimirlem29  32608  ismblfin  32620  itg2addnclem  32631  caures  32726