Theorem 3ad2ant1 967

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant1

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantr 271	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3	2	3adant2 965	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 927

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 929

This theorem is referenced by:  simp1l  970  simp1r  971  simp11  976  simp12  977  simp13  978  simp1ll  1009  simp1lr  1010  simp1rl  1011  simp1rr  1012  simp1l1  1039  simp1l2  1040  simp1l3  1041  simp1r1  1042  simp1r2  1043  simp1r3  1044  simp11l  1057  simp11r  1058  simp12l  1059  simp12r  1060  simp13l  1061  simp13r  1062  simp111  1075  simp112  1076  simp113  1077  simp121  1078  simp122  1079  simp123  1080  simp131  1081  simp132  1082  simp133  1083  3anim123i  1131  3jaao  1251  ceqsalt  2659  sbciegft  2883  reupick2  3301  ifbothdc  3443  frirrg  4201  breldmg  4673  fntpg  5104  funimaexglem  5131  fex2  5214  fvun1  5405  fprg  5519  fsnunfv  5537  fnfvima  5568  cocan1  5604  cocan2  5605  mpt2fvex  6011  poxp  6035  smoiso  6105  tfrlem5  6117  tfrlemibxssdm  6130  tfr1onlembfn  6147  tfri1dALT  6154  tfrcllembfn  6160  rdgon  6189  freccllem  6205  nnawordex  6327  mapxpen  6644  fidceq  6665  fidifsnen  6666  dif1en  6675  en2eqpr  6703  unsnfi  6709  unsnfidcex  6710  unsnfidcel  6711  fisseneq  6722  ordiso2  6808  updjud  6853  mkvprop  6901  mulcanenq0ec  7101  prltlu  7143  prarloclem3step  7152  prarloclem5  7156  ltasrg  7413  cnegexlem1  7754  addcan  7759  apcotr  8181  apadd1  8182  mulext1  8186  divdivap1  8287  divdivap2  8288  div2negap  8299  divneg2ap  8300  ltmulgt11  8422  ltdiv2  8445  squeeze0  8462  nndivtr  8562  nn0n0n1ge2  8915  zdivmul  8935  gtndiv  8940  eluzuzle  9126  eluzp1p1  9143  qdivcl  9227  irrmul  9231  rpgecl  9261  xaddass  9435  xltadd1  9442  xlt2add  9446  lbico1  9496  lbicc2  9550  zltaddlt1le  9572  uzsubsubfz  9610  elfz1b  9653  elfz0ubfz0  9685  fz0fzelfz0  9687  difelfzle  9694  difelfznle  9695  2ffzeq  9701  fzo1fzo0n0  9743  ubmelfzo  9760  fzonn0p1p1  9773  elfzom1p1elfzo  9774  elfzonelfzo  9790  subfzo0  9802  ceiqle  9869  ceilqle  9870  modqval  9880  flqpmodeq  9883  modq0  9885  negqmod0  9887  modqge0  9888  modqlt  9889  modqdiffl  9891  modqmulnn  9898  modqvalp1  9899  modqmuladdnn0  9924  qnegmod  9925  addmodid  9928  modfzo0difsn  9951  addmodlteq  9954  qexpclz  10107  expgt1  10124  expp1zap  10135  expm1ap  10136  expubnd  10143  bernneq2  10206  expnlbnd  10209  omgadd  10341  hashun  10344  fihashssdif  10357  hashdifpr  10359  fimaxq  10366  shftuz  10382  mulreap  10429  redivap  10439  imdivap  10446  resqrtcl  10593  xrmaxltsup  10817  xrmaxaddlem  10819  xrmaxadd  10820  xrlemininf  10830  xrminltinf  10831  climuni  10852  addcn2  10869  mulcn2  10871  efsub  11136  sin02gt0  11219  dvdsval2  11242  addmodlteqALT  11303  modremain  11372  fldivndvdslt  11378  mulgcdr  11450  gcddiv  11451  rpmulgcd  11458  rplpwr  11459  rppwr  11460  qredeq  11521  divgcdcoprmex  11527  cncongr1  11528  cncongr2  11529  dvdsnprmd  11550  euclemma  11568  prmexpb  11573  qnumdenbi  11613  hashgcdlem  11646  unennn  11653  setsex  11691  basgen  11948  2basgeng  11950  iuncld  11983  neipsm  12022  opnneissb  12023  opnssneib  12024  iscnp3  12070  cnprcl2k  12073  cnpnei  12086  cncnp2m  12098  cnptoprest  12106  sslm  12114  distspace  12137  0met  12186  blvalps  12190  blval  12191  ssblps  12227  ssbl  12228  blpnfctr  12241  blopn  12292  blnei  12294  bdxmet  12303  bdbl  12305  metcnp3  12309  tgqioo  12337  bdfind  12565