Theorem adantrl 478

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantrl	⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 286	1 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad2ant2l  508  ad2ant2rl  511  3ad2antr2  1163  3ad2antr3  1164  xordidc  1399  foco  5450  fvun1  5584  isocnv  5814  isores2  5816  f1oiso2  5830  offval  6092  xp2nd  6169  1stconst  6224  2ndconst  6225  tfrlem9  6322  nnmordi  6519  dom2lem  6774  fundmen  6808  mapen  6848  ssenen  6853  ltsonq  7399  ltexnqq  7409  genprndl  7522  genprndu  7523  ltpopr  7596  ltsopr  7597  ltexprlemm  7601  ltexprlemopl  7602  ltexprlemopu  7604  ltexprlemdisj  7607  ltexprlemfl  7610  ltexprlemfu  7612  mulcmpblnrlemg  7741  cnegexlem2  8135  muladd  8343  eqord1  8442  eqord2  8443  divadddivap  8686  ltmul12a  8819  lemul12b  8820  cju  8920  zextlt  9347  supinfneg  9597  infsupneg  9598  xrre  9822  ixxdisj  9905  iooshf  9954  icodisj  9994  iccshftr  9996  iccshftl  9998  iccdil  10000  icccntr  10002  iccf1o  10006  fzaddel  10061  fzsubel  10062  seq3caopr  10485  expineg2  10531  expsubap  10570  expnbnd  10646  facndiv  10721  hashfacen  10818  fprodeq0  11627  lcmdvds  12081  hashdvds  12223  eulerthlemh  12233  pceu  12297  pcqcl  12308  infpnlem1  12359  mhmpropd  12862  grplcan  12937  grplmulf1o  12949  dfgrp3mlem  12973  mulgfng  12992  mulgsubcl  13002  subsubg  13062  eqger  13088  subsubrg  13371  txlm  13864  blininf  14009  xmeter  14021  xmetresbl  14025  limcimo  14219