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  4277  frminex  5598  tz6.26i  6300  wfii  6302  tfr2ALT  8326  tfr3ALT  8327  opthreg  9515  unsnen  10451  axcnre  11062  addgt0  11610  addgegt0  11611  addgtge0  11612  addge0  11613  addgt0i  11663  addge0i  11664  addgegt0i  11665  add20i  11667  mulge0i  11671  recextlem1  11754  recne0  11796  recdiv  11834  rec11i  11869  recgt1  12025  prodgt0i  12036  xadddi2  13198  iccshftri  13389  iccshftli  13391  iccdili  13393  icccntri  13395  mulexpz  14011  expaddz  14015  m1expeven  14018  iexpcyc  14116  cnpart  15149  resqrex  15159  sqreulem  15269  amgm2  15279  rlim  15404  ello12  15425  elo12  15436  bpolylem  15957  ege2le3  15999  dvdslelem  16222  divalglem1  16307  divalglem6  16311  divalglem9  16314  gcdaddmlem  16437  sqnprm  16615  prmlem1  17021  prmlem2  17033  m1expaddsub  19412  psgnuni  19413  gzrngunitlem  21371  lmres  23216  zdis  24733  iihalf1  24853  lmclimf  25232  vitali  25542  ismbf  25557  ismbfcn  25558  mbfconst  25562  cncombf  25587  cnmbf  25588  limcfval  25801  dvnfre  25884  quotlem  26236  ulmval  26317  ulmpm  26320  abelthlem2  26370  abelthlem3  26371  abelthlem5  26373  abelthlem7  26376  efcvx  26387  logtayl  26597  logccv  26600  cxpcn3  26686  emcllem2  26935  zetacvg  26953  basellem5  27023  bposlem7  27229  chebbnd1lem3  27410  dchrisumlem3  27430  iscgrgd  28492  axcontlem2  28945  nv1  30657  blocnilem  30786  ipasslem8  30819  siii  30835  ubthlem1  30852  norm1  31231  hhshsslem2  31250  hoscli  31744  hodcli  31745  cnlnadjlem7  32055  adjbdln  32065  pjnmopi  32130  strlem1  32232  rexdiv  32913  tpr2rico  33946  qqhre  34054  signsply0  34585  subfacval3  35254  erdszelem4  35259  erdszelem8  35263  elmrsubrn  35585  rdgprc  35857  fwddifval  36227  fwddifnval  36228  exrecfnlem  37444  poimirlem29  37709  ismblfin  37721  itg2addnclem  37731  caures  37820  sswfaxreg  45104  nthrucw  47008  cjnpoly  47013  pgnbgreunbgrlem1  48237  pgnbgreunbgrlem4  48243  iooii  49042  icccldii  49043