Theorem 3ad2ant2 1009

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

Syntax hints:   → wi 4   ∧ w3a 968

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 970

This theorem is referenced by:  simp2l  1013  simp2r  1014  simp21  1020  simp22  1021  simp23  1022  simp2ll  1054  simp2lr  1055  simp2rl  1056  simp2rr  1057  simp2l1  1086  simp2l2  1087  simp2l3  1088  simp2r1  1089  simp2r2  1090  simp2r3  1091  simp21l  1104  simp21r  1105  simp22l  1106  simp22r  1107  simp23l  1108  simp23r  1109  simp211  1125  simp212  1126  simp213  1127  simp221  1128  simp222  1129  simp223  1130  simp231  1131  simp232  1132  simp233  1133  3anim123i  1174  3jaao  1298  ceqsalt  2752  vtoclgft  2776  vtoclegft  2798  ifbothdc  3552  frirrg  4328  elirr  4518  en2lp  4531  reg3exmidlemwe  4556  sotri3  5002  funtpg  5239  fnprg  5243  fntpg  5244  funimaexglem  5271  fnco  5296  fvun1  5552  oprssov  5983  caovimo  6035  rdgivallem  6349  fnsnsplitdc  6473  funresdfunsndc  6474  f1dom2g  6722  mapxpen  6814  ssfidc  6900  sbthlemi4  6925  ordiso2  7000  updjud  7047  difinfsn  7065  mkvprop  7122  endjudisj  7166  distrnqg  7328  distrnq0  7400  prarloclem5  7441  cauappcvgprlemlol  7588  cauappcvgprlemupu  7590  caucvgprlemlol  7611  caucvgprlemupu  7613  caucvgprprlemlol  7639  caucvgprprlemupu  7641  cnegexlem2  8074  apcotr  8505  apadd1  8506  mulext1  8510  div2negap  8631  ltdiv2  8782  nndivtr  8899  difgtsumgt  9260  zdivmul  9281  gtndiv  9286  fzind  9306  eluzuzle  9474  eluzp1p1  9491  peano2uz  9521  qdivcl  9581  irrmul  9585  ledivge1le  9662  xrre2  9757  xaddass  9805  xltadd1  9812  xlt2add  9816  ubioc1  9865  ubicc2  9921  zltaddlt1le  9943  uzsubsubfz  9982  elfz1b  10025  fzp1nel  10039  fz0fzdiffz0  10065  difelfzle  10069  elfzo0  10117  elfzonlteqm1  10145  fzonn0p1p1  10148  fzosplitprm1  10169  fzoshftral  10173  subfzo0  10177  ceiqle  10248  modqval  10259  modqvalr  10260  flqpmodeq  10262  modq0  10264  mulqmod0  10265  negqmod0  10266  modqge0  10267  modqlt  10268  modqelico  10269  modqdiffl  10270  modqmulnn  10277  modqvalp1  10278  modqmuladdnn0  10303  qnegmod  10304  addmodid  10307  q2submod  10320  modifeq2int  10321  modfzo0difsn  10330  addmodlteq  10333  omgadd  10715  hashun  10718  redivap  10816  imdivap  10823  xrmaxltsup  11199  xrmaxadd  11202  xrlemininf  11212  xrminltinf  11213  climuni  11234  mulcn2  11253  fsumsplitsnun  11360  prodfap0  11486  fprodabs  11557  efsub  11622  cos12dec  11708  dvdsmodexp  11735  summodnegmod  11762  divalglemex  11859  divalg  11861  modremain  11866  ndvdssub  11867  fldivndvdslt  11872  nndvdslegcd  11898  dfgcd2  11947  mulgcd  11949  mulgcdr  11951  gcddiv  11952  rplpwr  11960  rppwr  11961  qredeq  12028  divgcdcoprmex  12034  cncongr1  12035  cncongr2  12036  pw2dvdslemn  12097  hashgcdlem  12170  modprm0  12186  modprmn0modprm0  12188  pythagtriplem1  12197  pythagtriplem3  12199  pythagtriplem10  12201  pythagtriplem6  12202  pythagtriplem7  12203  pythagtriplem11  12206  pythagtriplem12  12207  pythagtriplem13  12208  pythagtriplem14  12209  pythagtriplem19  12214  pythagtrip  12215  dvdsprmpweqnn  12267  difsqpwdvds  12269  pcfaclem  12279  pcbc  12281  unennn  12330  mgmsscl  12592  ntrin  12764  elnei  12792  restco  12814  cnpnei  12859  cncnp2m  12871  sslm  12887  upxp  12912  blres  13074  metcnp3  13151  tgqioo  13187  ptolemy  13385  cxpcom  13497  logbgcd1irr  13525  logbprmirr  13530  lgslem1  13541  lgsneg  13565  lgsdilem  13568  lgsdir  13576  lgssq2  13582  lgsdirnn0  13588