Theorem adantrl 482

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 ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad2ant2l  512  ad2ant2rl  515  3ad2antr2  1194  3ad2antr3  1195  xordidc  1448  opabssxpd  4811  foco  5626  fvun1  5769  isocnv  6017  isores2  6019  f1oiso2  6033  offval  6310  xp2nd  6400  1stconst  6457  2ndconst  6458  tfrlem9  6590  nnmordi  6789  dom2lem  7058  fundmen  7094  mapen  7146  mapunen  7151  ssenen  7152  ltsonq  7765  ltexnqq  7775  genprndl  7888  genprndu  7889  ltpopr  7962  ltsopr  7963  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemdisj  7973  ltexprlemfl  7976  ltexprlemfu  7978  mulcmpblnrlemg  8107  cnegexlem2  8503  muladd  8712  eqord1  8812  eqord2  8813  divadddivap  9059  ltmul12a  9192  lemul12b  9193  cju  9293  zextlt  9742  supinfneg  10004  infsupneg  10005  xrre  10232  ixxdisj  10315  iooshf  10364  icodisj  10404  iccshftr  10406  iccshftl  10408  iccdil  10410  icccntr  10412  iccf1o  10417  fzaddel  10475  fzsubel  10476  seq3caopr  10945  seqcaoprg  10946  expineg2  10998  expsubap  11037  expnbnd  11114  facndiv  11191  hashfibclem  11296  hashfacen  11298  hashf1lem1  11299  ccatpfx  11487  swrdccatfn  11510  swrdccatin2  11515  fprodeq0  12400  lcmdvds  12873  hashdvds  13019  eulerthlemh  13029  pceu  13094  pcqcl  13105  infpnlem1  13158  4sqlem11  13200  mhmpropd  13822  subsubm  13839  grplcan  13916  grplmulf1o  13928  dfgrp3mlem  13952  mulgfng  13976  mulgsubcl  13988  subsubg  14049  eqger  14076  resghm  14112  conjghm  14128  subsubrng  14571  subsubrg  14602  issubassa2  15084  psrbagconf1o  15113  psrgrp  15125  txlm  15429  blininf  15574  xmeter  15586  xmetresbl  15590  limcimo  15815  dvdsppwf1o  16184  fsumdvdsmul  16186  sgmmul  16191  clwwlkn1loopb  16759