Theorem adantrr 483

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

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:  ad2ant2r  513  ad2ant2lr  514  dn1dc  973  3ad2antr1  1193  xordidc  1448  po2nr  4454  sotricim  4468  fmptco  5874  fvtp1g  5923  dff13  5974  fcof1o  5995  isocnv  6017  isores2  6019  isoini  6024  f1oiso2  6033  acexmidlemab  6079  ovmpodf  6220  offval  6310  xp1st  6399  1stconst  6457  cnvf1olem  6460  f1od2  6471  mpoxopoveq  6511  nnaordi  6781  nnmordi  6789  erinxp  6883  dom2lem  7058  fundmen  7094  pw2f1odclem  7134  mapen  7146  ssenen  7152  fidifsnen  7172  difinfsnlem  7439  fodjum  7486  cc2lem  7632  ltsonq  7765  lt2addnq  7771  lt2mulnq  7772  ltexnqq  7775  prarloclemarch2  7786  enq0sym  7799  genprndl  7888  genprndu  7889  prmuloc  7933  distrlem1prl  7949  distrlem1pru  7950  ltsopr  7963  ltexprlemdisj  7973  ltexprlemfl  7976  ltexprlemfu  7978  addcanprlemu  7982  ltaprg  7986  mulcmpblnrlemg  8107  recexgt0sr  8140  mul4  8458  2addsub  8540  muladd  8711  ltleadd  8774  eqord1  8811  eqord2  8812  divmulap3  9008  divcanap7  9052  divadddivap  9058  lemul2a  9190  lemul12b  9192  ltmuldiv2  9206  ltdivmul  9207  ltdivmul2  9209  ledivmul2  9211  lemuldiv2  9213  lt2msq  9217  cju  9292  zextlt  9740  xrlttr  10199  xrre3  10226  ixxdisj  10307  iooshf  10356  icodisj  10396  iccf1o  10409  zssinfcl  10667  seqf1og  10960  expsubap  11026  bcval5  11203  hashmap  11270  hashfacen  11286  seq3coll  11296  swrdswrdlem  11478  swrdccatin2  11503  sqrt0rlem  11771  lenegsq  11863  zsumdc  12153  fisum0diag2  12216  prodmodclem2  12346  zproddc  12348  ndvdsadd  12700  lcmdvds  12859  oddpwdclemdc  12953  hashdvds  13001  phisum  13021  pcqmul  13084  pcmpt  13124  4sqlemffi  13177  4sqlem11  13182  ballotfilemfc0  13234  ballotfilemfcc  13235  ennnfonelemex  13307  grpinvid1  13859  grpinvid2  13860  grplcan  13869  grpnpncan0  13903  dfgrp3mlem  13905  dfgrp3m  13906  grplactcnv  13909  0nsg  14019  eqger  14029  resghm  14065  conjghm  14081  znunit  14996  issubassa3  15014  issubassa2  15037  psrbagconf1o  15066  psrgrp  15078  eltg2  15156  ssnei2  15260  restopnb  15284  txdis1cn  15381  txlm  15382  elbl2ps  15495  elbl2  15496  blininf  15527  xmeter  15539  xmetresbl  15543  bdxmet  15604  metrest  15609  dedekindicc  15736  limcimo  15768  dvmptfsum  15828  plycolemc  15861  logdivlt  15999  dvdsppwf1o  16109  fsumdvdsmul  16111  sgmmul  16116  lgsquadlem1  16208  lgsquadlem2  16209  lgsquad2lem2  16213  upgriswlkdc  16613