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  sn0disj  4127  po2nr  4456  sotricim  4470  fmptco  5877  fvtp1g  5926  dff13  5977  fcof1o  5998  isocnv  6020  isores2  6022  isoini  6027  f1oiso2  6036  acexmidlemab  6082  ovmpodf  6223  offval  6314  xp1st  6403  1stconst  6461  cnvf1olem  6464  f1od2  6475  mpoxopoveq  6515  nnaordi  6785  nnmordi  6793  erinxp  6887  dom2lem  7063  fundmen  7099  pw2f1odclem  7139  mapen  7151  ssenen  7157  fidifsnen  7177  difinfsnlem  7446  fodjum  7493  cc2lem  7639  ltsonq  7772  lt2addnq  7778  lt2mulnq  7779  ltexnqq  7782  prarloclemarch2  7793  enq0sym  7806  genprndl  7895  genprndu  7896  prmuloc  7940  distrlem1prl  7956  distrlem1pru  7957  ltsopr  7970  ltexprlemdisj  7980  ltexprlemfl  7983  ltexprlemfu  7985  addcanprlemu  7989  ltaprg  7993  mulcmpblnrlemg  8114  recexgt0sr  8147  mul4  8466  2addsub  8548  muladd  8719  ltleadd  8782  eqord1  8819  eqord2  8820  divmulap3  9016  divcanap7  9060  divadddivap  9066  lemul2a  9198  lemul12b  9200  ltmuldiv2  9214  ltdivmul  9215  ltdivmul2  9217  ledivmul2  9219  lemuldiv2  9221  lt2msq  9225  cju  9300  zextlt  9750  xrlttr  10215  xrre3  10242  ixxdisj  10323  iooshf  10372  icodisj  10412  iccf1o  10425  zssinfcl  10683  seqf1og  10980  expsubap  11046  bcval5  11224  hashmap  11291  hashfacen  11307  seq3coll  11317  swrdswrdlem  11499  swrdccatin2  11524  sqrt0rlem  11792  lenegsq  11885  zsumdc  12177  fisum0diag2  12240  prodmodclem2  12370  zproddc  12372  ndvdsadd  12724  lcmdvds  12883  hashdvds  13029  phisum  13049  pcqmul  13112  pcmpt  13152  4sqlemffi  13205  4sqlem11  13210  ballotfilemfc0  13291  ballotfilemfcc  13292  ennnfonelemex  13364  grpinvid1  13917  grpinvid2  13918  grplcan  13927  grpnpncan0  13961  dfgrp3mlem  13963  dfgrp3m  13964  grplactcnv  13967  0nsg  14077  eqger  14087  resghm  14123  conjghm  14139  znunit  15104  issubassa3  15122  issubassa2  15145  psrbagconf1o  15179  psrgrp  15200  eltg2  15291  ssnei2  15395  restopnb  15419  txdis1cn  15516  txlm  15517  elbl2ps  15630  elbl2  15631  blininf  15662  xmeter  15674  xmetresbl  15678  bdxmet  15739  metrest  15744  dedekindicc  15871  limcimo  15903  dvmptfsum  15963  plycolemc  15996  logdivlt  16136  dvdsppwf1o  16295  fsumdvdsmul  16297  sgmmul  16302  bposlem1  16323  lgsquadlem1  16413  lgsquadlem2  16414  lgsquad2lem2  16418  upgriswlkdc  16818