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  6656  fnsnsplitdc  6782  funresdfunsndc  6783  mapsnd  6974  f1dom2g  7046  mapxpen  7152  ssfidc  7249  sbthlemi4  7282  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  9725  zdivmul  9747  gtndiv  9752  fzind  9772  eluzuzle  9946  eluzp1p1  9964  peano2uz  9999  qdivcl  10059  irrmul  10064  ledivge1le  10144  xrre2  10240  xaddass  10288  xltadd1  10295  xlt2add  10299  ubioc1  10348  ubicc2  10404  zltaddlt1le  10427  uzsubsubfz  10469  elfz1b  10514  fzp1nel  10528  fz0fzdiffz0  10554  difelfzle  10558  elfzo0  10610  elfzonlteqm1  10645  fzonn0p1p1  10648  fzosplitprm1  10670  fzoshftral  10674  subfzo0  10678  ceiqle  10771  modqval  10782  modqvalr  10783  flqpmodeq  10785  modq0  10787  mulqmod0  10788  negqmod0  10789  modqge0  10790  modqlt  10791  modqelico  10792  modqdiffl  10793  modqmulnn  10800  modqvalp1  10801  modqmuladdnn0  10826  qnegmod  10827  addmodid  10830  q2submod  10843  modifeq2int  10844  modfzo0difsn  10853  addmodlteq  10856  mulsubdivbinom2ap  11171  omgadd  11264  hashun  11267  ccatass  11398  lswccatn0lsw  11401  ccats1val2  11430  swrd00g  11443  swrdval2  11445  swrdlen  11446  swrdfv  11447  swrdfv0  11448  swrdnd  11453  swrdlen2  11456  swrdfv2  11457  swrdsbslen  11460  swrdspsleq  11461  ccatswrd  11464  pfxfv  11478  pfxn0  11482  pfxnd  11483  pfxsuff1eqwrdeq  11493  pfxpfx  11502  ccats1pfxeq  11508  ccatopth2  11511  wrd2ind  11517  pfxccatin12lem3  11526  pfxccat3  11528  swrdccat  11529  pfxccat3a  11532  redivap  11661  imdivap  11668  xrmaxltsup  12049  xrmaxadd  12052  xrlemininf  12062  xrminltinf  12063  climuni  12084  mulcn2  12103  fsumsplitsnun  12211  prodfap0  12337  fprodabs  12408  efsub  12473  cos12dec  12560  dvdsmodexp  12587  summodnegmod  12614  divalglemex  12714  divalg  12716  modremain  12721  ndvdssub  12722  fldivndvdslt  12729  bitsfzo  12747  nndvdslegcd  12767  dfgcd2  12816  mulgcd  12818  mulgcdr  12820  gcddiv  12821  rplpwr  12829  rppwr  12830  qredeq  12899  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  hashgcdlem  13045  modprm0  13062  modprmn0modprm0  13064  pythagtriplem1  13073  pythagtriplem3  13075  pythagtriplem10  13077  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem11  13082  pythagtriplem12  13083  pythagtriplem13  13084  pythagtriplem14  13085  pythagtriplem19  13090  pythagtrip  13091  dvdsprmpweqnn  13144  difsqpwdvds  13146  pcfaclem  13157  pcbc  13159  ballotfilemsgt1  13312  ballotfilemieq  13318  ballotfilemfrcn0  13331  unennn  13346  ptex  13677  imasaddvallemg  13695  fvprif  13723  mgmsscl  13740  insubm  13851  mulginvcom  14009  mulgassr  14022  mulgmodid  14023  quselbasg  14092  ghmnsgima  14130  gsumsncmn  14246  ringrng  14448  rmodislmodlem  14796  rmodislmod  14797  lssincl  14831  sralmod  14896  rnglidlmmgm  14942  rnglidlmsgrp  14943  rnglidlrng  14944  2idlcpblrng  14969  assa2ass  15118  assa2ass2  15119  aspid  15126  psrbaglesuppg  15166  psrbagaddclfi  15170  ntrin  15350  elnei  15378  restco  15400  cnpnei  15445  cncnp2m  15457  sslm  15473  upxp  15498  blres  15660  metcnp3  15737  tgqioo  15781  dvply1  15991  ptolemy  16051  cxpcom  16173  efnthr  16176  logbgcd1irr  16203  logbprmirr  16208  pellexlem1  16229  chtqwordi  16263  efchtqdvds  16265  ppiqwordi  16268  bcmono  16304  lgslem1  16324  lgsneg  16348  lgsdilem  16351  lgsdir  16359  lgssq2  16365  lgsdirnn0  16371  gausslemma2dlem1a  16382  2lgslem1a1  16410  incistruhgr  16536  upgrex  16549  uhgr2edg  16652  usgr2v1e2w  16692  issubgr2  16704  0uhgrsubgr  16711  subgrfun  16713  subgreldmiedg  16715  subumgredg2en  16717  iedginwlk  16803  uspgr2wlkeq2  16812  umgrclwwlkge2  16848  clwwlkext2edg  16868  clwwlknccat  16869  umgr2cwwk2dif  16870  umgr2cwwkdifex  16871  clwwlknonex2  16885