Theorem 3ad2ant2 1021

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simp2l  1025  simp2r  1026  simp21  1032  simp22  1033  simp23  1034  simp2ll  1066  simp2lr  1067  simp2rl  1068  simp2rr  1069  simp2l1  1098  simp2l2  1099  simp2l3  1100  simp2r1  1101  simp2r2  1102  simp2r3  1103  simp21l  1116  simp21r  1117  simp22l  1118  simp22r  1119  simp23l  1120  simp23r  1121  simp211  1137  simp212  1138  simp213  1139  simp221  1140  simp222  1141  simp223  1142  simp231  1143  simp232  1144  simp233  1145  3anim123i  1186  3jaao  1320  ceqsalt  2797  vtoclgft  2822  vtoclegft  2844  ifbothdc  3604  ifnebibdc  3614  frirrg  4396  elirr  4588  en2lp  4601  reg3exmidlemwe  4626  sotri3  5080  funtpg  5324  fnprg  5328  fntpg  5329  funimaexglem  5356  fnco  5383  fvun1  5644  oprssov  6087  caovimo  6139  rdgivallem  6466  fnsnsplitdc  6590  funresdfunsndc  6591  f1dom2g  6846  mapxpen  6944  ssfidc  7033  sbthlemi4  7061  ordiso2  7136  updjud  7183  difinfsn  7201  mkvprop  7259  endjudisj  7321  distrnqg  7499  distrnq0  7571  prarloclem5  7612  cauappcvgprlemlol  7759  cauappcvgprlemupu  7761  caucvgprlemlol  7782  caucvgprlemupu  7784  caucvgprprlemlol  7810  caucvgprprlemupu  7812  cnegexlem2  8247  apcotr  8679  apadd1  8680  mulext1  8684  div2negap  8807  ltdiv2  8959  nndivtr  9077  difgtsumgt  9441  zdivmul  9462  gtndiv  9467  fzind  9487  eluzuzle  9655  eluzp1p1  9673  peano2uz  9703  qdivcl  9763  irrmul  9767  ledivge1le  9847  xrre2  9942  xaddass  9990  xltadd1  9997  xlt2add  10001  ubioc1  10050  ubicc2  10106  zltaddlt1le  10128  uzsubsubfz  10168  elfz1b  10211  fzp1nel  10225  fz0fzdiffz0  10251  difelfzle  10255  elfzo0  10304  elfzonlteqm1  10337  fzonn0p1p1  10340  fzosplitprm1  10361  fzoshftral  10365  subfzo0  10369  ceiqle  10456  modqval  10467  modqvalr  10468  flqpmodeq  10470  modq0  10472  mulqmod0  10473  negqmod0  10474  modqge0  10475  modqlt  10476  modqelico  10477  modqdiffl  10478  modqmulnn  10485  modqvalp1  10486  modqmuladdnn0  10511  qnegmod  10512  addmodid  10515  q2submod  10528  modifeq2int  10529  modfzo0difsn  10538  addmodlteq  10541  mulsubdivbinom2ap  10854  omgadd  10945  hashun  10948  ccatass  11062  lswccatn0lsw  11065  ccats1val2  11090  redivap  11156  imdivap  11163  xrmaxltsup  11540  xrmaxadd  11543  xrlemininf  11553  xrminltinf  11554  climuni  11575  mulcn2  11594  fsumsplitsnun  11701  prodfap0  11827  fprodabs  11898  efsub  11963  cos12dec  12050  dvdsmodexp  12077  summodnegmod  12104  divalglemex  12204  divalg  12206  modremain  12211  ndvdssub  12212  fldivndvdslt  12219  bitsfzo  12237  nndvdslegcd  12257  dfgcd2  12306  mulgcd  12308  mulgcdr  12310  gcddiv  12311  rplpwr  12319  rppwr  12320  qredeq  12389  divgcdcoprmex  12395  cncongr1  12396  cncongr2  12397  pw2dvdslemn  12458  hashgcdlem  12531  modprm0  12548  modprmn0modprm0  12550  pythagtriplem1  12559  pythagtriplem3  12561  pythagtriplem10  12563  pythagtriplem6  12564  pythagtriplem7  12565  pythagtriplem11  12568  pythagtriplem12  12569  pythagtriplem13  12570  pythagtriplem14  12571  pythagtriplem19  12576  pythagtrip  12577  dvdsprmpweqnn  12630  difsqpwdvds  12632  pcfaclem  12643  pcbc  12645  unennn  12739  ptex  13067  imasaddvallemg  13118  fvprif  13146  mgmsscl  13164  insubm  13288  mulginvcom  13454  mulgassr  13467  mulgmodid  13468  quselbasg  13537  ghmnsgima  13575  ringrng  13769  rmodislmodlem  14083  rmodislmod  14084  lssincl  14118  sralmod  14183  rnglidlmmgm  14229  rnglidlmsgrp  14230  rnglidlrng  14231  2idlcpblrng  14256  psrbaglesuppg  14405  ntrin  14567  elnei  14595  restco  14617  cnpnei  14662  cncnp2m  14674  sslm  14690  upxp  14715  blres  14877  metcnp3  14954  tgqioo  14998  dvply1  15208  ptolemy  15267  cxpcom  15381  logbgcd1irr  15410  logbprmirr  15415  lgslem1  15448  lgsneg  15472  lgsdilem  15475  lgsdir  15483  lgssq2  15489  lgsdirnn0  15495  gausslemma2dlem1a  15506  2lgslem1a1  15534