Theorem 3ad2ant2 1014

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

Syntax hints:   → wi 4   ∧ w3a 973

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 975

This theorem is referenced by:  simp2l  1018  simp2r  1019  simp21  1025  simp22  1026  simp23  1027  simp2ll  1059  simp2lr  1060  simp2rl  1061  simp2rr  1062  simp2l1  1091  simp2l2  1092  simp2l3  1093  simp2r1  1094  simp2r2  1095  simp2r3  1096  simp21l  1109  simp21r  1110  simp22l  1111  simp22r  1112  simp23l  1113  simp23r  1114  simp211  1130  simp212  1131  simp213  1132  simp221  1133  simp222  1134  simp223  1135  simp231  1136  simp232  1137  simp233  1138  3anim123i  1179  3jaao  1303  ceqsalt  2756  vtoclgft  2780  vtoclegft  2802  ifbothdc  3557  frirrg  4333  elirr  4523  en2lp  4536  reg3exmidlemwe  4561  sotri3  5007  funtpg  5247  fnprg  5251  fntpg  5252  funimaexglem  5279  fnco  5304  fvun1  5560  oprssov  5992  caovimo  6044  rdgivallem  6358  fnsnsplitdc  6482  funresdfunsndc  6483  f1dom2g  6732  mapxpen  6824  ssfidc  6910  sbthlemi4  6935  ordiso2  7010  updjud  7057  difinfsn  7075  mkvprop  7132  endjudisj  7180  distrnqg  7342  distrnq0  7414  prarloclem5  7455  cauappcvgprlemlol  7602  cauappcvgprlemupu  7604  caucvgprlemlol  7625  caucvgprlemupu  7627  caucvgprprlemlol  7653  caucvgprprlemupu  7655  cnegexlem2  8088  apcotr  8519  apadd1  8520  mulext1  8524  div2negap  8645  ltdiv2  8796  nndivtr  8913  difgtsumgt  9274  zdivmul  9295  gtndiv  9300  fzind  9320  eluzuzle  9488  eluzp1p1  9505  peano2uz  9535  qdivcl  9595  irrmul  9599  ledivge1le  9676  xrre2  9771  xaddass  9819  xltadd1  9826  xlt2add  9830  ubioc1  9879  ubicc2  9935  zltaddlt1le  9957  uzsubsubfz  9996  elfz1b  10039  fzp1nel  10053  fz0fzdiffz0  10079  difelfzle  10083  elfzo0  10131  elfzonlteqm1  10159  fzonn0p1p1  10162  fzosplitprm1  10183  fzoshftral  10187  subfzo0  10191  ceiqle  10262  modqval  10273  modqvalr  10274  flqpmodeq  10276  modq0  10278  mulqmod0  10279  negqmod0  10280  modqge0  10281  modqlt  10282  modqelico  10283  modqdiffl  10284  modqmulnn  10291  modqvalp1  10292  modqmuladdnn0  10317  qnegmod  10318  addmodid  10321  q2submod  10334  modifeq2int  10335  modfzo0difsn  10344  addmodlteq  10347  omgadd  10730  hashun  10733  redivap  10831  imdivap  10838  xrmaxltsup  11214  xrmaxadd  11217  xrlemininf  11227  xrminltinf  11228  climuni  11249  mulcn2  11268  fsumsplitsnun  11375  prodfap0  11501  fprodabs  11572  efsub  11637  cos12dec  11723  dvdsmodexp  11750  summodnegmod  11777  divalglemex  11874  divalg  11876  modremain  11881  ndvdssub  11882  fldivndvdslt  11887  nndvdslegcd  11913  dfgcd2  11962  mulgcd  11964  mulgcdr  11966  gcddiv  11967  rplpwr  11975  rppwr  11976  qredeq  12043  divgcdcoprmex  12049  cncongr1  12050  cncongr2  12051  pw2dvdslemn  12112  hashgcdlem  12185  modprm0  12201  modprmn0modprm0  12203  pythagtriplem1  12212  pythagtriplem3  12214  pythagtriplem10  12216  pythagtriplem6  12217  pythagtriplem7  12218  pythagtriplem11  12221  pythagtriplem12  12222  pythagtriplem13  12223  pythagtriplem14  12224  pythagtriplem19  12229  pythagtrip  12230  dvdsprmpweqnn  12282  difsqpwdvds  12284  pcfaclem  12294  pcbc  12296  unennn  12345  mgmsscl  12608  insubm  12696  ntrin  12883  elnei  12911  restco  12933  cnpnei  12978  cncnp2m  12990  sslm  13006  upxp  13031  blres  13193  metcnp3  13270  tgqioo  13306  ptolemy  13504  cxpcom  13616  logbgcd1irr  13644  logbprmirr  13649  lgslem1  13660  lgsneg  13684  lgsdilem  13687  lgsdir  13695  lgssq2  13701  lgsdirnn0  13707