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  7375  updjud  7422  difinfsn  7440  mkvprop  7498  endjudisj  7566  distrnqg  7754  distrnq0  7826  prarloclem5  7867  cauappcvgprlemlol  8014  cauappcvgprlemupu  8016  caucvgprlemlol  8037  caucvgprlemupu  8039  caucvgprprlemlol  8065  caucvgprprlemupu  8067  cnegexlem2  8502  apcotr  8935  apadd1  8936  mulext1  8940  div2negap  9065  ltdiv2  9217  nndivtr  9346  difgtsumgt  9714  zdivmul  9736  gtndiv  9741  fzind  9761  eluzuzle  9930  eluzp1p1  9948  peano2uz  9983  qdivcl  10043  irrmul  10047  ledivge1le  10127  xrre2  10223  xaddass  10271  xltadd1  10278  xlt2add  10282  ubioc1  10331  ubicc2  10387  zltaddlt1le  10410  uzsubsubfz  10452  elfz1b  10497  fzp1nel  10511  fz0fzdiffz0  10537  difelfzle  10541  elfzo0  10593  elfzonlteqm1  10628  fzonn0p1p1  10631  fzosplitprm1  10653  fzoshftral  10657  subfzo0  10661  ceiqle  10750  modqval  10761  modqvalr  10762  flqpmodeq  10764  modq0  10766  mulqmod0  10767  negqmod0  10768  modqge0  10769  modqlt  10770  modqelico  10771  modqdiffl  10772  modqmulnn  10779  modqvalp1  10780  modqmuladdnn0  10805  qnegmod  10806  addmodid  10809  q2submod  10822  modifeq2int  10823  modfzo0difsn  10832  addmodlteq  10835  mulsubdivbinom2ap  11149  omgadd  11242  hashun  11245  ccatass  11376  lswccatn0lsw  11379  ccats1val2  11408  swrd00g  11421  swrdval2  11423  swrdlen  11424  swrdfv  11425  swrdfv0  11426  swrdnd  11431  swrdlen2  11434  swrdfv2  11435  swrdsbslen  11438  swrdspsleq  11439  ccatswrd  11442  pfxfv  11456  pfxn0  11460  pfxnd  11461  pfxsuff1eqwrdeq  11471  pfxpfx  11480  ccats1pfxeq  11486  ccatopth2  11489  wrd2ind  11495  pfxccatin12lem3  11504  pfxccat3  11506  swrdccat  11507  pfxccat3a  11510  redivap  11639  imdivap  11646  xrmaxltsup  12024  xrmaxadd  12027  xrlemininf  12037  xrminltinf  12038  climuni  12059  mulcn2  12078  fsumsplitsnun  12186  prodfap0  12312  fprodabs  12383  efsub  12448  cos12dec  12535  dvdsmodexp  12562  summodnegmod  12589  divalglemex  12689  divalg  12691  modremain  12696  ndvdssub  12697  fldivndvdslt  12704  bitsfzo  12722  nndvdslegcd  12742  dfgcd2  12791  mulgcd  12793  mulgcdr  12795  gcddiv  12796  rplpwr  12804  rppwr  12805  qredeq  12874  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  pw2dvdslemn  12943  hashgcdlem  13016  modprm0  13033  modprmn0modprm0  13035  pythagtriplem1  13044  pythagtriplem3  13046  pythagtriplem10  13048  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem11  13053  pythagtriplem12  13054  pythagtriplem13  13055  pythagtriplem14  13056  pythagtriplem19  13061  pythagtrip  13062  dvdsprmpweqnn  13115  difsqpwdvds  13117  pcfaclem  13128  pcbc  13130  ballotfilemsgt1  13254  ballotfilemieq  13260  ballotfilemfrcn0  13273  unennn  13288  ptex  13618  imasaddvallemg  13636  fvprif  13664  mgmsscl  13681  insubm  13792  mulginvcom  13950  mulgassr  13963  mulgmodid  13964  quselbasg  14033  ghmnsgima  14071  gsumsncmn  14156  ringrng  14341  rmodislmodlem  14687  rmodislmod  14688  lssincl  14722  sralmod  14787  rnglidlmmgm  14833  rnglidlmsgrp  14834  rnglidlrng  14835  2idlcpblrng  14860  assa2ass  15009  assa2ass2  15010  aspid  15017  psrbaglesuppg  15057  psrbagaddclfi  15061  ntrin  15225  elnei  15253  restco  15275  cnpnei  15320  cncnp2m  15332  sslm  15348  upxp  15373  blres  15535  metcnp3  15612  tgqioo  15656  dvply1  15866  ptolemy  15925  cxpcom  16040  logbgcd1irr  16069  logbprmirr  16074  pellexlem1  16091  lgslem1  16119  lgsneg  16143  lgsdilem  16146  lgsdir  16154  lgssq2  16160  lgsdirnn0  16166  gausslemma2dlem1a  16177  2lgslem1a1  16205  incistruhgr  16331  upgrex  16344  uhgr2edg  16447  usgr2v1e2w  16487  issubgr2  16499  0uhgrsubgr  16506  subgrfun  16508  subgreldmiedg  16510  subumgredg2en  16512  iedginwlk  16598  uspgr2wlkeq2  16607  umgrclwwlkge2  16643  clwwlkext2edg  16663  clwwlknccat  16664  umgr2cwwk2dif  16665  umgr2cwwkdifex  16666  clwwlknonex2  16680