Theorem adantrr 479

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

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 109	. 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:  ad2ant2r  509  ad2ant2lr  510  dn1dc  960  3ad2antr1  1162  xordidc  1399  po2nr  4311  sotricim  4325  fmptco  5684  fvtp1g  5726  dff13  5771  fcof1o  5792  isocnv  5814  isores2  5816  isoini  5821  f1oiso2  5830  acexmidlemab  5871  ovmpodf  6008  offval  6092  xp1st  6168  1stconst  6224  cnvf1olem  6227  f1od2  6238  mpoxopoveq  6243  nnaordi  6511  nnmordi  6519  erinxp  6611  dom2lem  6774  fundmen  6808  mapen  6848  ssenen  6853  fidifsnen  6872  difinfsnlem  7100  fodjum  7146  cc2lem  7267  ltsonq  7399  lt2addnq  7405  lt2mulnq  7406  ltexnqq  7409  prarloclemarch2  7420  enq0sym  7433  genprndl  7522  genprndu  7523  prmuloc  7567  distrlem1prl  7583  distrlem1pru  7584  ltsopr  7597  ltexprlemdisj  7607  ltexprlemfl  7610  ltexprlemfu  7612  addcanprlemu  7616  ltaprg  7620  mulcmpblnrlemg  7741  recexgt0sr  7774  mul4  8091  2addsub  8173  muladd  8343  ltleadd  8405  eqord1  8442  eqord2  8443  divmulap3  8636  divcanap7  8680  divadddivap  8686  lemul2a  8818  lemul12b  8820  ltmuldiv2  8834  ltdivmul  8835  ltdivmul2  8837  ledivmul2  8839  lemuldiv2  8841  lt2msq  8845  cju  8920  zextlt  9347  xrlttr  9797  xrre3  9824  ixxdisj  9905  iooshf  9954  icodisj  9994  iccf1o  10006  expsubap  10570  bcval5  10745  hashfacen  10818  seq3coll  10824  sqrt0rlem  11014  lenegsq  11106  zsumdc  11394  fisum0diag2  11457  prodmodclem2  11587  zproddc  11589  ndvdsadd  11938  zssinfcl  11951  lcmdvds  12081  oddpwdclemdc  12175  hashdvds  12223  phisum  12242  pcqmul  12305  pcmpt  12343  ennnfonelemex  12417  grpinvid1  12929  grpinvid2  12930  grplcan  12937  grpnpncan0  12971  dfgrp3mlem  12973  dfgrp3m  12974  grplactcnv  12977  0nsg  13079  eqger  13088  eltg2  13638  ssnei2  13742  restopnb  13766  txdis1cn  13863  txlm  13864  elbl2ps  13977  elbl2  13978  blininf  14009  xmeter  14021  xmetresbl  14025  bdxmet  14086  metrest  14091  dedekindicc  14196  limcimo  14219