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  4495  elirr  4688  en2lp  4701  reg3exmidlemwe  4726  sotri3  5186  funtpg  5432  fnprg  5436  fntpg  5437  funimaexglem  5464  fnco  5491  fresaunres2disj  5570  fvun1  5769  oprssov  6231  caovimo  6283  suppsnopdc  6490  funsssuppss  6498  rdgivallem  6652  fnsnsplitdc  6778  funresdfunsndc  6779  mapsnd  6970  f1dom2g  7042  mapxpen  7148  ssfidc  7245  sbthlemi4  7277  ordiso2  7376  updjud  7423  difinfsn  7441  mkvprop  7499  endjudisj  7567  distrnqg  7755  distrnq0  7827  prarloclem5  7868  cauappcvgprlemlol  8015  cauappcvgprlemupu  8017  caucvgprlemlol  8038  caucvgprlemupu  8040  caucvgprprlemlol  8066  caucvgprprlemupu  8068  cnegexlem2  8504  apcotr  8938  apadd1  8939  mulext1  8943  div2negap  9068  ltdiv2  9220  nndivtr  9349  difgtsumgt  9719  zdivmul  9741  gtndiv  9746  fzind  9766  eluzuzle  9940  eluzp1p1  9958  peano2uz  9993  qdivcl  10053  irrmul  10058  ledivge1le  10138  xrre2  10234  xaddass  10282  xltadd1  10289  xlt2add  10293  ubioc1  10342  ubicc2  10398  zltaddlt1le  10421  uzsubsubfz  10463  elfz1b  10508  fzp1nel  10522  fz0fzdiffz0  10548  difelfzle  10552  elfzo0  10604  elfzonlteqm1  10639  fzonn0p1p1  10642  fzosplitprm1  10664  fzoshftral  10668  subfzo0  10672  ceiqle  10765  modqval  10776  modqvalr  10777  flqpmodeq  10779  modq0  10781  mulqmod0  10782  negqmod0  10783  modqge0  10784  modqlt  10785  modqelico  10786  modqdiffl  10787  modqmulnn  10794  modqvalp1  10795  modqmuladdnn0  10820  qnegmod  10821  addmodid  10824  q2submod  10837  modifeq2int  10838  modfzo0difsn  10847  addmodlteq  10850  mulsubdivbinom2ap  11165  omgadd  11258  hashun  11261  ccatass  11392  lswccatn0lsw  11395  ccats1val2  11424  swrd00g  11437  swrdval2  11439  swrdlen  11440  swrdfv  11441  swrdfv0  11442  swrdnd  11447  swrdlen2  11450  swrdfv2  11451  swrdsbslen  11454  swrdspsleq  11455  ccatswrd  11458  pfxfv  11472  pfxn0  11476  pfxnd  11477  pfxsuff1eqwrdeq  11487  pfxpfx  11496  ccats1pfxeq  11502  ccatopth2  11505  wrd2ind  11511  pfxccatin12lem3  11520  pfxccat3  11522  swrdccat  11523  pfxccat3a  11526  redivap  11655  imdivap  11662  xrmaxltsup  12043  xrmaxadd  12046  xrlemininf  12056  xrminltinf  12057  climuni  12078  mulcn2  12097  fsumsplitsnun  12205  prodfap0  12331  fprodabs  12402  efsub  12467  cos12dec  12554  dvdsmodexp  12581  summodnegmod  12608  divalglemex  12708  divalg  12710  modremain  12715  ndvdssub  12716  fldivndvdslt  12723  bitsfzo  12741  nndvdslegcd  12761  dfgcd2  12810  mulgcd  12812  mulgcdr  12814  gcddiv  12815  rplpwr  12823  rppwr  12824  qredeq  12893  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  hashgcdlem  13039  modprm0  13056  modprmn0modprm0  13058  pythagtriplem1  13067  pythagtriplem3  13069  pythagtriplem10  13071  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem11  13076  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem14  13079  pythagtriplem19  13084  pythagtrip  13085  dvdsprmpweqnn  13138  difsqpwdvds  13140  pcfaclem  13151  pcbc  13153  ballotfilemsgt1  13306  ballotfilemieq  13312  ballotfilemfrcn0  13325  unennn  13340  ptex  13671  imasaddvallemg  13689  fvprif  13717  mgmsscl  13734  insubm  13845  mulginvcom  14003  mulgassr  14016  mulgmodid  14017  quselbasg  14086  ghmnsgima  14124  gsumsncmn  14240  ringrng  14425  rmodislmodlem  14771  rmodislmod  14772  lssincl  14806  sralmod  14871  rnglidlmmgm  14917  rnglidlmsgrp  14918  rnglidlrng  14919  2idlcpblrng  14944  assa2ass  15093  assa2ass2  15094  aspid  15101  psrbaglesuppg  15141  psrbagaddclfi  15145  ntrin  15316  elnei  15344  restco  15366  cnpnei  15411  cncnp2m  15423  sslm  15439  upxp  15464  blres  15626  metcnp3  15703  tgqioo  15747  dvply1  15957  ptolemy  16017  cxpcom  16135  logbgcd1irr  16164  logbprmirr  16169  pellexlem1  16190  chtqwordi  16224  efchtqdvds  16226  ppiqwordi  16229  bcmono  16265  lgslem1  16285  lgsneg  16309  lgsdilem  16312  lgsdir  16320  lgssq2  16326  lgsdirnn0  16332  gausslemma2dlem1a  16343  2lgslem1a1  16371  incistruhgr  16497  upgrex  16510  uhgr2edg  16613  usgr2v1e2w  16653  issubgr2  16665  0uhgrsubgr  16672  subgrfun  16674  subgreldmiedg  16676  subumgredg2en  16678  iedginwlk  16764  uspgr2wlkeq2  16773  umgrclwwlkge2  16809  clwwlkext2edg  16829  clwwlknccat  16830  umgr2cwwk2dif  16831  umgr2cwwkdifex  16832  clwwlknonex2  16846