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  1189  3ad2antr3  1190  xordidc  1443  opabssxpd  4762  foco  5570  fvun1  5712  isocnv  5952  isores2  5954  f1oiso2  5968  offval  6243  xp2nd  6329  1stconst  6386  2ndconst  6387  tfrlem9  6485  nnmordi  6684  dom2lem  6945  fundmen  6981  mapen  7032  ssenen  7037  ltsonq  7618  ltexnqq  7628  genprndl  7741  genprndu  7742  ltpopr  7815  ltsopr  7816  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemdisj  7826  ltexprlemfl  7829  ltexprlemfu  7831  mulcmpblnrlemg  7960  cnegexlem2  8355  muladd  8563  eqord1  8663  eqord2  8664  divadddivap  8907  ltmul12a  9040  lemul12b  9041  cju  9141  zextlt  9572  supinfneg  9829  infsupneg  9830  xrre  10055  ixxdisj  10138  iooshf  10187  icodisj  10227  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  iccf1o  10239  fzaddel  10294  fzsubel  10295  seq3caopr  10758  seqcaoprg  10759  expineg2  10811  expsubap  10850  expnbnd  10926  facndiv  11002  hashfacen  11101  ccatpfx  11286  swrdccatfn  11309  swrdccatin2  11314  fprodeq0  12183  lcmdvds  12656  hashdvds  12798  eulerthlemh  12808  pceu  12873  pcqcl  12884  infpnlem1  12937  4sqlem11  12979  mhmpropd  13554  subsubm  13571  grplcan  13650  grplmulf1o  13662  dfgrp3mlem  13686  mulgfng  13716  mulgsubcl  13728  subsubg  13789  eqger  13816  resghm  13852  conjghm  13868  subsubrng  14234  subsubrg  14265  psrgrp  14705  txlm  15009  blininf  15154  xmeter  15166  xmetresbl  15170  limcimo  15395  dvdsppwf1o  15719  fsumdvdsmul  15721  sgmmul  15726  clwwlkn1loopb  16277