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  4291  frminex  5617  tz6.26i  6321  wfii  6323  tfr2ALT  8369  tfr3ALT  8370  opthreg  9571  unsnen  10506  axcnre  11117  addgt0  11664  addgegt0  11665  addgtge0  11666  addge0  11667  addgt0i  11717  addge0i  11718  addgegt0i  11719  add20i  11721  mulge0i  11725  recextlem1  11808  recne0  11850  recdiv  11888  rec11i  11923  recgt1  12079  prodgt0i  12090  xadddi2  13257  iccshftri  13448  iccshftli  13450  iccdili  13452  icccntri  13454  mulexpz  14067  expaddz  14071  m1expeven  14074  iexpcyc  14172  cnpart  15206  resqrex  15216  sqreulem  15326  amgm2  15336  rlim  15461  ello12  15482  elo12  15493  bpolylem  16014  ege2le3  16056  dvdslelem  16279  divalglem1  16364  divalglem6  16368  divalglem9  16371  gcdaddmlem  16494  sqnprm  16672  prmlem1  17078  prmlem2  17090  m1expaddsub  19428  psgnuni  19429  gzrngunitlem  21349  lmres  23187  zdis  24705  iihalf1  24825  lmclimf  25204  vitali  25514  ismbf  25529  ismbfcn  25530  mbfconst  25534  cncombf  25559  cnmbf  25560  limcfval  25773  dvnfre  25856  quotlem  26208  ulmval  26289  ulmpm  26292  abelthlem2  26342  abelthlem3  26343  abelthlem5  26345  abelthlem7  26348  efcvx  26359  logtayl  26569  logccv  26572  cxpcn3  26658  emcllem2  26907  zetacvg  26925  basellem5  26995  bposlem7  27201  chebbnd1lem3  27382  dchrisumlem3  27402  iscgrgd  28440  axcontlem2  28892  nv1  30604  blocnilem  30733  ipasslem8  30766  siii  30782  ubthlem1  30799  norm1  31178  hhshsslem2  31197  hoscli  31691  hodcli  31692  cnlnadjlem7  32002  adjbdln  32012  pjnmopi  32077  strlem1  32179  rexdiv  32846  tpr2rico  33902  qqhre  34010  signsply0  34542  subfacval3  35176  erdszelem4  35181  erdszelem8  35185  elmrsubrn  35507  rdgprc  35782  fwddifval  36150  fwddifnval  36151  exrecfnlem  37367  poimirlem29  37643  ismblfin  37655  itg2addnclem  37665  caures  37754  sswfaxreg  44977  cjnpoly  46890  pgnbgreunbgrlem1  48103  pgnbgreunbgrlem4  48109  iooii  48906  icccldii  48907