Theorem 3ad2ant2 1008

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

Syntax hints:   → wi 4   ∧ w3a 967

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 969

This theorem is referenced by:  simp2l  1012  simp2r  1013  simp21  1019  simp22  1020  simp23  1021  simp2ll  1053  simp2lr  1054  simp2rl  1055  simp2rr  1056  simp2l1  1085  simp2l2  1086  simp2l3  1087  simp2r1  1088  simp2r2  1089  simp2r3  1090  simp21l  1103  simp21r  1104  simp22l  1105  simp22r  1106  simp23l  1107  simp23r  1108  simp211  1124  simp212  1125  simp213  1126  simp221  1127  simp222  1128  simp223  1129  simp231  1130  simp232  1131  simp233  1132  3anim123i  1173  3jaao  1297  ceqsalt  2747  vtoclgft  2771  vtoclegft  2793  ifbothdc  3547  frirrg  4322  elirr  4512  en2lp  4525  reg3exmidlemwe  4550  sotri3  4996  funtpg  5233  fnprg  5237  fntpg  5238  funimaexglem  5265  fnco  5290  fvun1  5546  oprssov  5974  caovimo  6026  rdgivallem  6340  fnsnsplitdc  6464  funresdfunsndc  6465  f1dom2g  6713  mapxpen  6805  ssfidc  6891  sbthlemi4  6916  ordiso2  6991  updjud  7038  difinfsn  7056  mkvprop  7113  endjudisj  7157  distrnqg  7319  distrnq0  7391  prarloclem5  7432  cauappcvgprlemlol  7579  cauappcvgprlemupu  7581  caucvgprlemlol  7602  caucvgprlemupu  7604  caucvgprprlemlol  7630  caucvgprprlemupu  7632  cnegexlem2  8065  apcotr  8496  apadd1  8497  mulext1  8501  div2negap  8622  ltdiv2  8773  nndivtr  8890  difgtsumgt  9251  zdivmul  9272  gtndiv  9277  fzind  9297  eluzuzle  9465  eluzp1p1  9482  peano2uz  9512  qdivcl  9572  irrmul  9576  ledivge1le  9653  xrre2  9748  xaddass  9796  xltadd1  9803  xlt2add  9807  ubioc1  9856  ubicc2  9912  zltaddlt1le  9934  uzsubsubfz  9972  elfz1b  10015  fzp1nel  10029  fz0fzdiffz0  10055  difelfzle  10059  elfzo0  10107  elfzonlteqm1  10135  fzonn0p1p1  10138  fzosplitprm1  10159  fzoshftral  10163  subfzo0  10167  ceiqle  10238  modqval  10249  modqvalr  10250  flqpmodeq  10252  modq0  10254  mulqmod0  10255  negqmod0  10256  modqge0  10257  modqlt  10258  modqelico  10259  modqdiffl  10260  modqmulnn  10267  modqvalp1  10268  modqmuladdnn0  10293  qnegmod  10294  addmodid  10297  q2submod  10310  modifeq2int  10311  modfzo0difsn  10320  addmodlteq  10323  omgadd  10704  hashun  10707  redivap  10802  imdivap  10809  xrmaxltsup  11185  xrmaxadd  11188  xrlemininf  11198  xrminltinf  11199  climuni  11220  mulcn2  11239  fsumsplitsnun  11346  prodfap0  11472  fprodabs  11543  efsub  11608  cos12dec  11694  dvdsmodexp  11721  summodnegmod  11748  divalglemex  11844  divalg  11846  modremain  11851  ndvdssub  11852  fldivndvdslt  11857  nndvdslegcd  11883  dfgcd2  11932  mulgcd  11934  mulgcdr  11936  gcddiv  11937  rplpwr  11945  rppwr  11946  qredeq  12007  divgcdcoprmex  12013  cncongr1  12014  cncongr2  12015  pw2dvdslemn  12074  hashgcdlem  12147  modprm0  12163  modprmn0modprm0  12165  pythagtriplem1  12174  pythagtriplem3  12176  pythagtriplem10  12178  pythagtriplem6  12179  pythagtriplem7  12180  pythagtriplem11  12183  pythagtriplem12  12184  pythagtriplem13  12185  pythagtriplem14  12186  pythagtriplem19  12191  pythagtrip  12192  dvdsprmpweqnn  12244  difsqpwdvds  12246  pcfaclem  12256  pcbc  12258  unennn  12267  ntrin  12665  elnei  12693  restco  12715  cnpnei  12760  cncnp2m  12772  sslm  12788  upxp  12813  blres  12975  metcnp3  13052  tgqioo  13088  ptolemy  13286  cxpcom  13398  logbgcd1irr  13426  logbprmirr  13431