Theorem 3ad2ant2 1022

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 1018	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  simp2l  1026  simp2r  1027  simp21  1033  simp22  1034  simp23  1035  simp2ll  1067  simp2lr  1068  simp2rl  1069  simp2rr  1070  simp2l1  1099  simp2l2  1100  simp2l3  1101  simp2r1  1102  simp2r2  1103  simp2r3  1104  simp21l  1117  simp21r  1118  simp22l  1119  simp22r  1120  simp23l  1121  simp23r  1122  simp211  1138  simp212  1139  simp213  1140  simp221  1141  simp222  1142  simp223  1143  simp231  1144  simp232  1145  simp233  1146  3anim123i  1187  3jaao  1321  ceqsalt  2800  vtoclgft  2825  vtoclegft  2849  ifbothdc  3610  ifnebibdc  3620  frirrg  4405  elirr  4597  en2lp  4610  reg3exmidlemwe  4635  sotri3  5090  funtpg  5334  fnprg  5338  fntpg  5339  funimaexglem  5366  fnco  5393  fvun1  5658  oprssov  6101  caovimo  6153  rdgivallem  6480  fnsnsplitdc  6604  funresdfunsndc  6605  f1dom2g  6860  mapxpen  6960  ssfidc  7049  sbthlemi4  7077  ordiso2  7152  updjud  7199  difinfsn  7217  mkvprop  7275  endjudisj  7338  distrnqg  7520  distrnq0  7592  prarloclem5  7633  cauappcvgprlemlol  7780  cauappcvgprlemupu  7782  caucvgprlemlol  7803  caucvgprlemupu  7805  caucvgprprlemlol  7831  caucvgprprlemupu  7833  cnegexlem2  8268  apcotr  8700  apadd1  8701  mulext1  8705  div2negap  8828  ltdiv2  8980  nndivtr  9098  difgtsumgt  9462  zdivmul  9483  gtndiv  9488  fzind  9508  eluzuzle  9676  eluzp1p1  9694  peano2uz  9724  qdivcl  9784  irrmul  9788  ledivge1le  9868  xrre2  9963  xaddass  10011  xltadd1  10018  xlt2add  10022  ubioc1  10071  ubicc2  10127  zltaddlt1le  10149  uzsubsubfz  10189  elfz1b  10232  fzp1nel  10246  fz0fzdiffz0  10272  difelfzle  10276  elfzo0  10328  elfzonlteqm1  10361  fzonn0p1p1  10364  fzosplitprm1  10385  fzoshftral  10389  subfzo0  10393  ceiqle  10480  modqval  10491  modqvalr  10492  flqpmodeq  10494  modq0  10496  mulqmod0  10497  negqmod0  10498  modqge0  10499  modqlt  10500  modqelico  10501  modqdiffl  10502  modqmulnn  10509  modqvalp1  10510  modqmuladdnn0  10535  qnegmod  10536  addmodid  10539  q2submod  10552  modifeq2int  10553  modfzo0difsn  10562  addmodlteq  10565  mulsubdivbinom2ap  10878  omgadd  10969  hashun  10972  ccatass  11087  lswccatn0lsw  11090  ccats1val2  11115  swrd00g  11125  swrdval2  11127  swrdlen  11128  swrdfv  11129  swrdfv0  11130  swrdnd  11135  swrdlen2  11138  swrdfv2  11139  swrdsbslen  11142  swrdspsleq  11143  ccatswrd  11146  pfxfv  11160  pfxn0  11164  pfxnd  11165  pfxsuff1eqwrdeq  11175  pfxpfx  11184  ccats1pfxeq  11190  ccatopth2  11193  wrd2ind  11199  redivap  11260  imdivap  11267  xrmaxltsup  11644  xrmaxadd  11647  xrlemininf  11657  xrminltinf  11658  climuni  11679  mulcn2  11698  fsumsplitsnun  11805  prodfap0  11931  fprodabs  12002  efsub  12067  cos12dec  12154  dvdsmodexp  12181  summodnegmod  12208  divalglemex  12308  divalg  12310  modremain  12315  ndvdssub  12316  fldivndvdslt  12323  bitsfzo  12341  nndvdslegcd  12361  dfgcd2  12410  mulgcd  12412  mulgcdr  12414  gcddiv  12415  rplpwr  12423  rppwr  12424  qredeq  12493  divgcdcoprmex  12499  cncongr1  12500  cncongr2  12501  pw2dvdslemn  12562  hashgcdlem  12635  modprm0  12652  modprmn0modprm0  12654  pythagtriplem1  12663  pythagtriplem3  12665  pythagtriplem10  12667  pythagtriplem6  12668  pythagtriplem7  12669  pythagtriplem11  12672  pythagtriplem12  12673  pythagtriplem13  12674  pythagtriplem14  12675  pythagtriplem19  12680  pythagtrip  12681  dvdsprmpweqnn  12734  difsqpwdvds  12736  pcfaclem  12747  pcbc  12749  unennn  12843  ptex  13171  imasaddvallemg  13222  fvprif  13250  mgmsscl  13268  insubm  13392  mulginvcom  13558  mulgassr  13571  mulgmodid  13572  quselbasg  13641  ghmnsgima  13679  ringrng  13873  rmodislmodlem  14187  rmodislmod  14188  lssincl  14222  sralmod  14287  rnglidlmmgm  14333  rnglidlmsgrp  14334  rnglidlrng  14335  2idlcpblrng  14360  psrbaglesuppg  14509  ntrin  14671  elnei  14699  restco  14721  cnpnei  14766  cncnp2m  14778  sslm  14794  upxp  14819  blres  14981  metcnp3  15058  tgqioo  15102  dvply1  15312  ptolemy  15371  cxpcom  15485  logbgcd1irr  15514  logbprmirr  15519  lgslem1  15552  lgsneg  15576  lgsdilem  15579  lgsdir  15587  lgssq2  15593  lgsdirnn0  15599  gausslemma2dlem1a  15610  2lgslem1a1  15638  incistruhgr  15761  upgrex  15774