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  1165  3ad2antr3  1166  xordidc  1410  foco  5487  fvun1  5623  isocnv  5854  isores2  5856  f1oiso2  5870  offval  6138  xp2nd  6219  1stconst  6274  2ndconst  6275  tfrlem9  6372  nnmordi  6569  dom2lem  6826  fundmen  6860  mapen  6902  ssenen  6907  ltsonq  7458  ltexnqq  7468  genprndl  7581  genprndu  7582  ltpopr  7655  ltsopr  7656  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemdisj  7666  ltexprlemfl  7669  ltexprlemfu  7671  mulcmpblnrlemg  7800  cnegexlem2  8195  muladd  8403  eqord1  8502  eqord2  8503  divadddivap  8746  ltmul12a  8879  lemul12b  8880  cju  8980  zextlt  9409  supinfneg  9660  infsupneg  9661  xrre  9886  ixxdisj  9969  iooshf  10018  icodisj  10058  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  iccf1o  10070  fzaddel  10125  fzsubel  10126  seq3caopr  10566  seqcaoprg  10567  expineg2  10619  expsubap  10658  expnbnd  10734  facndiv  10810  hashfacen  10907  fprodeq0  11760  lcmdvds  12217  hashdvds  12359  eulerthlemh  12369  pceu  12433  pcqcl  12444  infpnlem1  12497  4sqlem11  12539  mhmpropd  13038  subsubm  13055  grplcan  13134  grplmulf1o  13146  dfgrp3mlem  13170  mulgfng  13194  mulgsubcl  13206  subsubg  13267  eqger  13294  resghm  13330  conjghm  13346  subsubrng  13710  subsubrg  13741  txlm  14447  blininf  14592  xmeter  14604  xmetresbl  14608  limcimo  14819