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  8503  apcotr  8937  apadd1  8938  mulext1  8942  div2negap  9067  ltdiv2  9219  nndivtr  9348  difgtsumgt  9718  zdivmul  9740  gtndiv  9745  fzind  9765  eluzuzle  9939  eluzp1p1  9957  peano2uz  9992  qdivcl  10052  irrmul  10057  ledivge1le  10137  xrre2  10233  xaddass  10281  xltadd1  10288  xlt2add  10292  ubioc1  10341  ubicc2  10397  zltaddlt1le  10420  uzsubsubfz  10462  elfz1b  10507  fzp1nel  10521  fz0fzdiffz0  10547  difelfzle  10551  elfzo0  10603  elfzonlteqm1  10638  fzonn0p1p1  10641  fzosplitprm1  10663  fzoshftral  10667  subfzo0  10671  ceiqle  10763  modqval  10774  modqvalr  10775  flqpmodeq  10777  modq0  10779  mulqmod0  10780  negqmod0  10781  modqge0  10782  modqlt  10783  modqelico  10784  modqdiffl  10785  modqmulnn  10792  modqvalp1  10793  modqmuladdnn0  10818  qnegmod  10819  addmodid  10822  q2submod  10835  modifeq2int  10836  modfzo0difsn  10845  addmodlteq  10848  mulsubdivbinom2ap  11163  omgadd  11256  hashun  11259  ccatass  11390  lswccatn0lsw  11393  ccats1val2  11422  swrd00g  11435  swrdval2  11437  swrdlen  11438  swrdfv  11439  swrdfv0  11440  swrdnd  11445  swrdlen2  11448  swrdfv2  11449  swrdsbslen  11452  swrdspsleq  11453  ccatswrd  11456  pfxfv  11470  pfxn0  11474  pfxnd  11475  pfxsuff1eqwrdeq  11485  pfxpfx  11494  ccats1pfxeq  11500  ccatopth2  11503  wrd2ind  11509  pfxccatin12lem3  11518  pfxccat3  11520  swrdccat  11521  pfxccat3a  11524  redivap  11653  imdivap  11660  xrmaxltsup  12040  xrmaxadd  12043  xrlemininf  12053  xrminltinf  12054  climuni  12075  mulcn2  12094  fsumsplitsnun  12202  prodfap0  12328  fprodabs  12399  efsub  12464  cos12dec  12551  dvdsmodexp  12578  summodnegmod  12605  divalglemex  12705  divalg  12707  modremain  12712  ndvdssub  12713  fldivndvdslt  12720  bitsfzo  12738  nndvdslegcd  12758  dfgcd2  12807  mulgcd  12809  mulgcdr  12811  gcddiv  12812  rplpwr  12820  rppwr  12821  qredeq  12890  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  hashgcdlem  13036  modprm0  13053  modprmn0modprm0  13055  pythagtriplem1  13064  pythagtriplem3  13066  pythagtriplem10  13068  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem11  13073  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem14  13076  pythagtriplem19  13081  pythagtrip  13082  dvdsprmpweqnn  13135  difsqpwdvds  13137  pcfaclem  13148  pcbc  13150  ballotfilemsgt1  13303  ballotfilemieq  13309  ballotfilemfrcn0  13322  unennn  13337  ptex  13667  imasaddvallemg  13685  fvprif  13713  mgmsscl  13730  insubm  13841  mulginvcom  13999  mulgassr  14012  mulgmodid  14013  quselbasg  14082  ghmnsgima  14120  gsumsncmn  14205  ringrng  14390  rmodislmodlem  14736  rmodislmod  14737  lssincl  14771  sralmod  14836  rnglidlmmgm  14882  rnglidlmsgrp  14883  rnglidlrng  14884  2idlcpblrng  14909  assa2ass  15058  assa2ass2  15059  aspid  15066  psrbaglesuppg  15106  psrbagaddclfi  15110  ntrin  15274  elnei  15302  restco  15324  cnpnei  15369  cncnp2m  15381  sslm  15397  upxp  15422  blres  15584  metcnp3  15661  tgqioo  15705  dvply1  15915  ptolemy  15975  cxpcom  16093  logbgcd1irr  16122  logbprmirr  16127  pellexlem1  16148  ppiqwordi  16174  bcmono  16202  lgslem1  16217  lgsneg  16241  lgsdilem  16244  lgsdir  16252  lgssq2  16258  lgsdirnn0  16264  gausslemma2dlem1a  16275  2lgslem1a1  16303  incistruhgr  16429  upgrex  16442  uhgr2edg  16545  usgr2v1e2w  16585  issubgr2  16597  0uhgrsubgr  16604  subgrfun  16606  subgreldmiedg  16608  subumgredg2en  16610  iedginwlk  16696  uspgr2wlkeq2  16705  umgrclwwlkge2  16741  clwwlkext2edg  16761  clwwlknccat  16762  umgr2cwwk2dif  16763  umgr2cwwkdifex  16764  clwwlknonex2  16778