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  4333  frminex  5667  tz6.26i  6371  wfii  6374  wfr3OLD  8376  tfr2ALT  8439  tfr3ALT  8440  opthreg  9655  unsnen  10590  axcnre  11201  addgt0  11746  addgegt0  11747  addgtge0  11748  addge0  11749  addgt0i  11799  addge0i  11800  addgegt0i  11801  add20i  11803  mulge0i  11807  recextlem1  11890  recne0  11932  recdiv  11970  rec11i  12005  recgt1  12161  prodgt0i  12172  xadddi2  13335  iccshftri  13523  iccshftli  13525  iccdili  13527  icccntri  13529  mulexpz  14139  expaddz  14143  m1expeven  14146  iexpcyc  14242  cnpart  15275  resqrex  15285  sqreulem  15394  amgm2  15404  rlim  15527  ello12  15548  elo12  15559  bpolylem  16080  ege2le3  16122  dvdslelem  16342  divalglem1  16427  divalglem6  16431  divalglem9  16434  gcdaddmlem  16557  sqnprm  16735  prmlem1  17141  prmlem2  17153  m1expaddsub  19530  psgnuni  19531  gzrngunitlem  21467  lmres  23323  zdis  24851  iihalf1  24971  lmclimf  25351  vitali  25661  ismbf  25676  ismbfcn  25677  mbfconst  25681  cncombf  25706  cnmbf  25707  limcfval  25921  dvnfre  26004  quotlem  26356  ulmval  26437  ulmpm  26440  abelthlem2  26490  abelthlem3  26491  abelthlem5  26493  abelthlem7  26496  efcvx  26507  logtayl  26716  logccv  26719  cxpcn3  26805  emcllem2  27054  zetacvg  27072  basellem5  27142  bposlem7  27348  chebbnd1lem3  27529  dchrisumlem3  27549  iscgrgd  28535  axcontlem2  28994  nv1  30703  blocnilem  30832  ipasslem8  30865  siii  30881  ubthlem1  30898  norm1  31277  hhshsslem2  31296  hoscli  31790  hodcli  31791  cnlnadjlem7  32101  adjbdln  32111  pjnmopi  32176  strlem1  32278  rexdiv  32892  tpr2rico  33872  qqhre  33982  signsply0  34544  subfacval3  35173  erdszelem4  35178  erdszelem8  35182  elmrsubrn  35504  rdgprc  35775  fwddifval  36143  fwddifnval  36144  exrecfnlem  37361  poimirlem29  37635  ismblfin  37647  itg2addnclem  37657  caures  37746  iooii  48713  icccldii  48714