Theorem 3ad2ant2 1050

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
3ad2ant2	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3	2	3adant1 1046	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

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

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp2l  1054  simp2r  1055  simp21  1061  simp22  1062  simp23  1063  simp2ll  1095  simp2lr  1096  simp2rl  1097  simp2rr  1098  simp2l1  1127  simp2l2  1128  simp2l3  1129  simp2r1  1130  simp2r2  1131  simp2r3  1132  simp21l  1145  simp21r  1146  simp22l  1147  simp22r  1148  simp23l  1149  simp23r  1150  simp211  1166  simp212  1167  simp213  1168  simp221  1169  simp222  1170  simp223  1171  simp231  1172  simp232  1173  simp233  1174  3anim123i  1215  3jaao  1349  ceqsalt  2848  vtoclgft  2873  vtoclegft  2897  ifbothdc  3675  ifnebibdc  3686  ifprdc  3819  frirrg  4497  elirr  4690  en2lp  4703  reg3exmidlemwe  4728  sotri3  5189  funtpg  5435  fnprg  5439  fntpg  5440  funimaexglem  5467  fnco  5494  fresaunres2disj  5573  fvun1  5772  oprssov  6234  caovimo  6286  suppsnopdc  6494  funsssuppss  6502  rdgivallem  6657  fnsnsplitdc  6783  funresdfunsndc  6784  mapsnd  6976  f1dom2g  7048  mapxpen  7154  ssfidc  7251  sbthlemi4  7284  snopfsupp  7306  ordiso2  7381  updjud  7428  difinfsn  7446  mkvprop  7504  endjudisj  7572  distrnqg  7760  distrnq0  7832  prarloclem5  7873  cauappcvgprlemlol  8020  cauappcvgprlemupu  8022  caucvgprlemlol  8043  caucvgprlemupu  8045  caucvgprprlemlol  8071  caucvgprprlemupu  8073  cnegexlem2  8509  apcotr  8943  apadd1  8944  mulext1  8948  div2negap  9073  ltdiv2  9225  nndivtr  9355  difgtsumgt  9723  zdivmul  9746  gtndiv  9751  fzind  9771  eluzuzle  9945  eluzp1p1  9963  peano2uz  9998  qdivcl  10058  irrmul  10063  ledivge1le  10143  xrre2  10239  xaddass  10287  xltadd1  10294  xlt2add  10298  ubioc1  10347  ubicc2  10403  zltaddlt1le  10426  uzsubsubfz  10468  elfz1b  10513  fzp1nel  10527  fz0fzdiffz0  10553  difelfzle  10557  elfzo0  10609  elfzonlteqm1  10644  fzonn0p1p1  10647  fzosplitprm1  10669  fzoshftral  10673  subfzo0  10677  ceiqle  10770  modqval  10781  modqvalr  10782  flqpmodeq  10784  modq0  10786  mulqmod0  10787  negqmod0  10788  modqge0  10789  modqlt  10790  modqelico  10791  modqdiffl  10792  modqmulnn  10799  modqvalp1  10800  modqmuladdnn0  10825  qnegmod  10826  addmodid  10829  q2submod  10842  modifeq2int  10843  modfzo0difsn  10852  addmodlteq  10855  mulsubdivbinom2ap  11170  omgadd  11263  hashun  11266  ccatass  11397  lswccatn0lsw  11400  ccats1val2  11429  swrd00g  11442  swrdval2  11444  swrdlen  11445  swrdfv  11446  swrdfv0  11447  swrdnd  11452  swrdlen2  11455  swrdfv2  11456  swrdsbslen  11459  swrdspsleq  11460  ccatswrd  11463  pfxfv  11477  pfxn0  11481  pfxnd  11482  pfxsuff1eqwrdeq  11492  pfxpfx  11501  ccats1pfxeq  11507  ccatopth2  11510  wrd2ind  11516  pfxccatin12lem3  11525  pfxccat3  11527  swrdccat  11528  pfxccat3a  11531  redivap  11660  imdivap  11667  xrmaxltsup  12048  xrmaxadd  12051  xrlemininf  12061  xrminltinf  12062  climuni  12083  mulcn2  12102  fsumsplitsnun  12210  prodfap0  12336  fprodabs  12407  efsub  12472  cos12dec  12559  dvdsmodexp  12586  summodnegmod  12613  divalglemex  12713  divalg  12715  modremain  12720  ndvdssub  12721  fldivndvdslt  12728  bitsfzo  12746  nndvdslegcd  12766  dfgcd2  12815  mulgcd  12817  mulgcdr  12819  gcddiv  12820  rplpwr  12828  rppwr  12829  qredeq  12898  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  hashgcdlem  13044  modprm0  13061  modprmn0modprm0  13063  pythagtriplem1  13072  pythagtriplem3  13074  pythagtriplem10  13076  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem11  13081  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem14  13084  pythagtriplem19  13089  pythagtrip  13090  dvdsprmpweqnn  13143  difsqpwdvds  13145  pcfaclem  13156  pcbc  13158  ballotfilemsgt1  13311  ballotfilemieq  13317  ballotfilemfrcn0  13330  unennn  13345  ptex  13676  imasaddvallemg  13694  fvprif  13722  mgmsscl  13739  insubm  13850  mulginvcom  14008  mulgassr  14021  mulgmodid  14022  quselbasg  14091  ghmnsgima  14129  gsumsncmn  14245  ringrng  14447  rmodislmodlem  14795  rmodislmod  14796  lssincl  14830  sralmod  14895  rnglidlmmgm  14941  rnglidlmsgrp  14942  rnglidlrng  14943  2idlcpblrng  14968  assa2ass  15117  assa2ass2  15118  aspid  15125  psrbaglesuppg  15170  psrbagaddclfi  15173  ntrin  15367  elnei  15395  restco  15417  cnpnei  15462  cncnp2m  15474  sslm  15490  upxp  15515  blres  15677  metcnp3  15754  tgqioo  15798  dvply1  16008  ptolemy  16068  cxpcom  16190  efnthr  16193  logbgcd1irr  16220  logbprmirr  16225  pellexlem1  16246  chtqwordi  16280  efchtqdvds  16282  ppiqwordi  16285  bcmono  16321  lgslem1  16341  lgsneg  16365  lgsdilem  16368  lgsdir  16376  lgssq2  16382  lgsdirnn0  16388  gausslemma2dlem1a  16399  2lgslem1a1  16427  incistruhgr  16553  upgrex  16566  uhgr2edg  16669  usgr2v1e2w  16709  issubgr2  16721  0uhgrsubgr  16728  subgrfun  16730  subgreldmiedg  16732  subumgredg2en  16734  iedginwlk  16820  uspgr2wlkeq2  16829  umgrclwwlkge2  16865  clwwlkext2edg  16885  clwwlknccat  16886  umgr2cwwk2dif  16887  umgr2cwwkdifex  16888  clwwlknonex2  16902