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  1187  3ad2antr3  1188  xordidc  1441  foco  5561  fvun1  5702  isocnv  5941  isores2  5943  f1oiso2  5957  offval  6232  xp2nd  6318  1stconst  6373  2ndconst  6374  tfrlem9  6471  nnmordi  6670  dom2lem  6931  fundmen  6967  mapen  7015  ssenen  7020  ltsonq  7596  ltexnqq  7606  genprndl  7719  genprndu  7720  ltpopr  7793  ltsopr  7794  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemdisj  7804  ltexprlemfl  7807  ltexprlemfu  7809  mulcmpblnrlemg  7938  cnegexlem2  8333  muladd  8541  eqord1  8641  eqord2  8642  divadddivap  8885  ltmul12a  9018  lemul12b  9019  cju  9119  zextlt  9550  supinfneg  9802  infsupneg  9803  xrre  10028  ixxdisj  10111  iooshf  10160  icodisj  10200  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  iccf1o  10212  fzaddel  10267  fzsubel  10268  seq3caopr  10729  seqcaoprg  10730  expineg2  10782  expsubap  10821  expnbnd  10897  facndiv  10973  hashfacen  11071  ccatpfx  11248  swrdccatfn  11271  swrdccatin2  11276  fprodeq0  12143  lcmdvds  12616  hashdvds  12758  eulerthlemh  12768  pceu  12833  pcqcl  12844  infpnlem1  12897  4sqlem11  12939  mhmpropd  13514  subsubm  13531  grplcan  13610  grplmulf1o  13622  dfgrp3mlem  13646  mulgfng  13676  mulgsubcl  13688  subsubg  13749  eqger  13776  resghm  13812  conjghm  13828  subsubrng  14193  subsubrg  14224  psrgrp  14664  txlm  14968  blininf  15113  xmeter  15125  xmetresbl  15129  limcimo  15354  dvdsppwf1o  15678  fsumdvdsmul  15680  sgmmul  15685