Theorem mpanl12 699

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  reuun1  4257  frminex  5569  tz6.26i  6250  wfii  6253  wfr3OLD  8158  tfr2ALT  8221  tfr3ALT  8222  opthreg  9352  unsnen  10308  axcnre  10919  addgt0  11459  addgegt0  11460  addgtge0  11461  addge0  11462  addgt0i  11512  addge0i  11513  addgegt0i  11514  add20i  11516  mulge0i  11520  recextlem1  11603  recne0  11644  recdiv  11679  rec11i  11714  recgt1  11869  prodgt0i  11880  xadddi2  13028  iccshftri  13216  iccshftli  13218  iccdili  13220  icccntri  13222  mulexpz  13819  expaddz  13823  m1expeven  13826  iexpcyc  13919  cnpart  14947  resqrex  14958  sqreulem  15067  amgm2  15077  rlim  15200  ello12  15221  elo12  15232  bpolylem  15754  ege2le3  15795  dvdslelem  16014  divalglem1  16099  divalglem6  16103  divalglem9  16106  gcdaddmlem  16227  sqnprm  16403  prmlem1  16805  prmlem2  16817  m1expaddsub  19102  psgnuni  19103  gzrngunitlem  20659  lmres  22447  zdis  23975  iihalf1  24090  lmclimf  24464  vitali  24773  ismbf  24788  ismbfcn  24789  mbfconst  24793  cncombf  24818  cnmbf  24819  limcfval  25032  dvnfre  25112  quotlem  25456  ulmval  25535  ulmpm  25538  abelthlem2  25587  abelthlem3  25588  abelthlem5  25590  abelthlem7  25593  efcvx  25604  logtayl  25811  logccv  25814  cxpcn3  25897  emcllem2  26142  zetacvg  26160  basellem5  26230  bposlem7  26434  chebbnd1lem3  26615  dchrisumlem3  26635  iscgrgd  26870  axcontlem2  27329  nv1  29031  blocnilem  29160  ipasslem8  29193  siii  29209  ubthlem1  29226  norm1  29605  hhshsslem2  29624  hoscli  30118  hodcli  30119  cnlnadjlem7  30429  adjbdln  30439  pjnmopi  30504  strlem1  30606  rexdiv  31194  tpr2rico  31856  qqhre  31964  signsply0  32524  subfacval3  33145  erdszelem4  33150  erdszelem8  33154  elmrsubrn  33476  rdgprc  33764  fwddifval  34458  fwddifnval  34459  exrecfnlem  35544  poimirlem29  35800  ismblfin  35812  itg2addnclem  35822  caures  35912  iooii  46178  icccldii  46179