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  966  3ad2antr1  1186  xordidc  1441  po2nr  4401  sotricim  4415  fmptco  5806  fvtp1g  5854  dff13  5901  fcof1o  5922  isocnv  5944  isores2  5946  isoini  5951  f1oiso2  5960  acexmidlemab  6004  ovmpodf  6145  offval  6235  xp1st  6320  1stconst  6378  cnvf1olem  6381  f1od2  6392  mpoxopoveq  6397  nnaordi  6667  nnmordi  6675  erinxp  6769  dom2lem  6936  fundmen  6972  pw2f1odclem  7008  mapen  7020  ssenen  7025  fidifsnen  7045  difinfsnlem  7282  fodjum  7329  cc2lem  7468  ltsonq  7601  lt2addnq  7607  lt2mulnq  7608  ltexnqq  7611  prarloclemarch2  7622  enq0sym  7635  genprndl  7724  genprndu  7725  prmuloc  7769  distrlem1prl  7785  distrlem1pru  7786  ltsopr  7799  ltexprlemdisj  7809  ltexprlemfl  7812  ltexprlemfu  7814  addcanprlemu  7818  ltaprg  7822  mulcmpblnrlemg  7943  recexgt0sr  7976  mul4  8294  2addsub  8376  muladd  8546  ltleadd  8609  eqord1  8646  eqord2  8647  divmulap3  8840  divcanap7  8884  divadddivap  8890  lemul2a  9022  lemul12b  9024  ltmuldiv2  9038  ltdivmul  9039  ltdivmul2  9041  ledivmul2  9043  lemuldiv2  9045  lt2msq  9049  cju  9124  zextlt  9555  xrlttr  10008  xrre3  10035  ixxdisj  10116  iooshf  10165  icodisj  10205  iccf1o  10217  zssinfcl  10469  seqf1og  10760  expsubap  10826  bcval5  11002  hashfacen  11076  seq3coll  11082  swrdswrdlem  11257  swrdccatin2  11282  sqrt0rlem  11535  lenegsq  11627  zsumdc  11916  fisum0diag2  11979  prodmodclem2  12109  zproddc  12111  ndvdsadd  12463  lcmdvds  12622  oddpwdclemdc  12716  hashdvds  12764  phisum  12784  pcqmul  12847  pcmpt  12887  4sqlemffi  12940  4sqlem11  12945  ennnfonelemex  13006  grpinvid1  13606  grpinvid2  13607  grplcan  13616  grpnpncan0  13650  dfgrp3mlem  13652  dfgrp3m  13653  grplactcnv  13656  0nsg  13772  eqger  13782  resghm  13818  conjghm  13834  znunit  14644  psrgrp  14670  eltg2  14748  ssnei2  14852  restopnb  14876  txdis1cn  14973  txlm  14974  elbl2ps  15087  elbl2  15088  blininf  15119  xmeter  15131  xmetresbl  15135  bdxmet  15196  metrest  15201  dedekindicc  15328  limcimo  15360  dvmptfsum  15420  plycolemc  15453  dvdsppwf1o  15684  fsumdvdsmul  15686  sgmmul  15691  lgsquadlem1  15777  lgsquadlem2  15778  lgsquad2lem2  15782  upgriswlkdc  16132