Theorem 3ad2ant1 1003

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 274	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3	2	3adant2 1001	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 963

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

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

This theorem is referenced by:  simp1l  1006  simp1r  1007  simp11  1012  simp12  1013  simp13  1014  simp1ll  1045  simp1lr  1046  simp1rl  1047  simp1rr  1048  simp1l1  1075  simp1l2  1076  simp1l3  1077  simp1r1  1078  simp1r2  1079  simp1r3  1080  simp11l  1093  simp11r  1094  simp12l  1095  simp12r  1096  simp13l  1097  simp13r  1098  simp111  1111  simp112  1112  simp113  1113  simp121  1114  simp122  1115  simp123  1116  simp131  1117  simp132  1118  simp133  1119  3anim123i  1167  3jaao  1287  ceqsalt  2715  sbciegft  2943  reupick2  3367  ifbothdc  3509  frirrg  4280  breldmg  4753  fntpg  5187  funimaexglem  5214  fex2  5299  fvun1  5495  fprg  5611  fsnunfv  5629  fnfvima  5660  cocan1  5696  cocan2  5697  mpoeq3dv  5845  mpofvex  6109  poxp  6137  smoiso  6207  tfrlem5  6219  tfrlemibxssdm  6232  tfr1onlembfn  6249  tfri1dALT  6256  tfrcllembfn  6262  rdgon  6291  freccllem  6307  nnawordex  6432  mapxpen  6750  fidceq  6771  fidifsnen  6772  dif1en  6781  en2eqpr  6809  unsnfi  6815  unsnfidcex  6816  unsnfidcel  6817  fisseneq  6828  ordiso2  6928  updjud  6975  mkvprop  7040  endjudisj  7083  xpdjuen  7091  mulcanenq0ec  7277  prltlu  7319  prarloclem3step  7328  prarloclem5  7332  ltasrg  7602  cnegexlem1  7961  addcan  7966  apcotr  8393  apadd1  8394  mulext1  8398  divdivap1  8507  divdivap2  8508  div2negap  8519  divneg2ap  8520  ltmulgt11  8646  ltdiv2  8669  squeeze0  8686  nndivtr  8786  nn0n0n1ge2  9145  zdivmul  9165  gtndiv  9170  eluzuzle  9358  eluzp1p1  9375  qdivcl  9462  irrmul  9466  rpgecl  9499  xaddass  9682  xltadd1  9689  xlt2add  9693  lbico1  9743  lbicc2  9797  zltaddlt1le  9820  uzsubsubfz  9858  elfz1b  9901  elfz0ubfz0  9933  fz0fzelfz0  9935  difelfzle  9942  difelfznle  9943  2ffzeq  9949  fzo1fzo0n0  9991  ubmelfzo  10008  fzonn0p1p1  10021  elfzom1p1elfzo  10022  elfzonelfzo  10038  subfzo0  10050  ceiqle  10117  ceilqle  10118  modqval  10128  flqpmodeq  10131  modq0  10133  negqmod0  10135  modqge0  10136  modqlt  10137  modqdiffl  10139  modqmulnn  10146  modqvalp1  10147  modqmuladdnn0  10172  qnegmod  10173  addmodid  10176  modfzo0difsn  10199  addmodlteq  10202  qexpclz  10345  expgt1  10362  expp1zap  10373  expm1ap  10374  expubnd  10381  bernneq2  10444  expnlbnd  10447  omgadd  10580  hashun  10583  fihashssdif  10596  hashdifpr  10598  fimaxq  10605  shftuz  10621  mulreap  10668  redivap  10678  imdivap  10685  resqrtcl  10833  xrmaxltsup  11059  xrmaxaddlem  11061  xrmaxadd  11062  xrlemininf  11072  xrminltinf  11073  climuni  11094  addcn2  11111  mulcn2  11113  efsub  11424  sin02gt0  11506  cos12dec  11510  dvdsval2  11532  addmodlteqALT  11593  modremain  11662  fldivndvdslt  11668  mulgcdr  11742  gcddiv  11743  rpmulgcd  11750  rplpwr  11751  rppwr  11752  qredeq  11813  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  dvdsnprmd  11842  euclemma  11860  prmexpb  11865  qnumdenbi  11906  hashgcdlem  11939  unennn  11946  setsex  12030  basgen  12288  2basgeng  12290  iuncld  12323  neipsm  12362  opnneissb  12363  opnssneib  12364  iscnp3  12411  cnprcl2k  12414  cnpnei  12427  cncnp2m  12439  cnptoprest  12447  sslm  12455  upxp  12480  cnmpt22  12502  distspace  12543  0met  12592  blvalps  12596  blval  12597  ssblps  12633  ssbl  12634  blpnfctr  12647  blopn  12698  blnei  12700  bdxmet  12709  bdbl  12711  metcnp3  12719  tgqioo  12755  ptolemy  12953  sinq12gt0  12959  sincosq1eq  12968  rpcxpadd  13034  cxpmul  13041  rplogbval  13070  logbleb  13086  logbgcd1irr  13092  logbprmirr  13097  bdfind  13315