Theorem 3ad2ant1 1049

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
3ad2ant1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

Proof of Theorem 3ad2ant1

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantr 276	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3	2	3adant2 1047	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp1l  1052  simp1r  1053  simp11  1058  simp12  1059  simp13  1060  simp1ll  1091  simp1lr  1092  simp1rl  1093  simp1rr  1094  simp1l1  1121  simp1l2  1122  simp1l3  1123  simp1r1  1124  simp1r2  1125  simp1r3  1126  simp11l  1139  simp11r  1140  simp12l  1141  simp12r  1142  simp13l  1143  simp13r  1144  simp111  1157  simp112  1158  simp113  1159  simp121  1160  simp122  1161  simp123  1162  simp131  1163  simp132  1164  simp133  1165  3anim123i  1215  3jaao  1349  ceqsalt  2848  sbciegft  3082  reupick2  3519  ifbothdc  3675  ifprdc  3819  frirrg  4497  breldmg  4989  fntpg  5440  funimaexglem  5467  fex2  5559  fresaunres2disj  5573  fvun1  5772  fprg  5901  fsnunfv  5919  fnfvima  5956  cocan1  5996  cocan2  5997  mpoeq3dv  6157  fovcld  6196  fvmpopr2d  6228  funexw  6345  mpofvex  6445  poxp  6472  suppval1  6483  suppvalfng  6484  suppvalfn  6485  suppimacnvfn  6490  suppsnopdc  6494  smoiso  6578  tfrlem5  6590  tfrlemibxssdm  6603  tfr1onlembfn  6620  tfri1dALT  6627  tfrcllembfn  6633  rdgon  6662  freccllem  6678  nnawordex  6807  1dom1el  7113  mapxpen  7154  fidceq  7177  fidifsnen  7178  dif1en  7189  en2eqpr  7220  unsnfi  7232  unsnfidcex  7233  unsnfidcel  7234  fisseneq  7248  snopfsupp  7306  ordiso2  7381  updjud  7428  mkvprop  7504  endjudisj  7572  xpdjuen  7580  mulcanenq0ec  7818  prltlu  7860  prarloclem3step  7869  prarloclem5  7873  ltasrg  8143  cnegexlem1  8508  addcan  8513  apcotr  8943  apadd1  8944  mulext1  8948  divdivap1  9061  divdivap2  9062  div2negap  9073  divneg2ap  9074  ltmulgt11  9202  ltdiv2  9225  squeeze0  9242  nndivtr  9355  nn0n0n1ge2  9724  zdivmul  9746  gtndiv  9751  eluzuzle  9945  eluzp1p1  9963  qdivcl  10058  irrmul  10063  rpgecl  10099  xaddass  10287  xltadd1  10294  xlt2add  10298  lbico1  10348  lbicc2  10402  zltaddlt1le  10426  uzsubsubfz  10468  elfz1b  10513  elfz0ubfz0  10548  fz0fzelfz0  10550  difelfzle  10557  difelfznle  10558  2ffzeq  10564  fzo1fzo0n0  10611  ubmelfzo  10634  fzonn0p1p1  10647  elfzom1p1elfzo  10648  elfzonelfzo  10664  subfzo0  10677  ceiqle  10770  ceilqle  10771  modqval  10781  flqpmodeq  10784  modq0  10786  negqmod0  10788  modqge0  10789  modqlt  10790  modqdiffl  10792  modqmulnn  10799  modqvalp1  10800  modqmuladdnn0  10825  qnegmod  10826  addmodid  10829  modfzo0difsn  10852  addmodlteq  10855  qexpclz  11017  expgt1  11034  expp1zap  11045  expm1ap  11046  expubnd  11053  bernneq2  11119  expnlbnd  11122  mulsubdivbinom2ap  11170  omgadd  11263  hashun  11266  fihashssdif  11280  hashdifpr  11282  fimaxq  11291  ccatval2  11387  ccatval3  11388  ccatval1lsw  11393  ccatval21sw  11394  ccatass  11397  ccatw2s1leng  11427  ccats1val2  11429  ccat2s1fvwd  11436  fzowrddc  11440  swrdval  11441  swrdclg  11443  swrdval2  11444  swrdnd  11452  swrdlen2  11455  swrdfv2  11456  ccatswrd  11463  pfxn0  11481  pfxsuff1eqwrdeq  11492  swrdswrdlem  11497  ccats1pfxeq  11507  ccats1pfxeqrex  11508  ccatopth2  11510  wrd2ind  11516  pfxccatin12lem3  11525  pfxccat3  11527  swrdccat  11528  pfxccatpfx2  11530  pfxccat3a  11531  swrdccat3b  11533  pfxccatid  11534  ccats1pfxeqbi  11535  shftuz  11603  mulreap  11650  redivap  11660  imdivap  11667  resqrtcl  11816  xrmaxltsup  12048  xrmaxaddlem  12050  xrmaxadd  12051  xrlemininf  12061  xrminltinf  12062  climuni  12083  addcn2  12100  mulcn2  12102  efsub  12472  sin02gt0  12555  cos12dec  12559  dvdsval2  12581  addmodlteqALT  12650  modremain  12720  fldivndvdslt  12728  mulgcdr  12819  gcddiv  12820  rpmulgcd  12827  rplpwr  12828  rppwr  12829  nnminle  12836  qredeq  12898  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  dvdsnprmd  12927  euclemma  12949  prmexpb  12954  qnumdenbi  12996  eulerth  13039  fermltl  13040  prmdiv  13041  hashgcdlem  13044  odzcllem  13049  vfermltl  13058  reumodprminv  13060  modprm0  13061  modprmn0modprm0  13063  coprimeprodsq  13064  pythagtriplem1  13072  pythagtriplem3  13074  pythagtriplem4  13075  pythagtriplem10  13076  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem8  13079  pythagtriplem9  13080  pythagtriplem11  13081  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem14  13084  pythagtriplem15  13085  pythagtriplem16  13086  pythagtriplem17  13087  pythagtriplem19  13089  pythagtrip  13090  pcpremul  13100  pcdvdsb  13127  dvdsprmpweqnn  13143  dvdsprmpweqle  13144  difsqpwdvds  13145  pcfaclem  13156  pcbc  13158  4sqlem12  13209  ballotfilemsgt1  13311  ballotfilemieq  13317  ballotfilemfrcn0  13330  unennn  13345  nninfdc  13401  setsex  13441  f1ocpbllem  13689  imasaddfnlemg  13693  imasaddvallemg  13694  ercpbl  13710  erlecpbl  13711  qusaddvallemg  13712  fvprif  13722  xpsfrnel2  13725  plusfvalg  13741  imasmnd  13818  insubm  13850  grpidrcan  13928  grpidlcan  13929  grpsubpropd2  13968  imasgrp2  13971  imasgrp  13972  mulgnnsubcl  13995  mulgnn0subcl  13996  mulgsubcl  13997  mulgaddcom  14007  mulginvcom  14008  mulgnnass  14018  mulgassr  14021  mulgpropdg  14025  submmulg  14027  subgcl  14045  subgsubcl  14046  subgsub  14047  subgmulg  14049  nsgconj  14067  ghmsub  14112  ghmrn  14118  ghmeqker  14132  f1ghm0to0  14133  ablinvadd  14203  ablsub4  14206  abladdsub4  14207  subcmnd  14226  imasabl  14229  gsumconstcmn  14265  pwsinvg  14321  rngcl  14349  imasrng  14361  rng1zrlem  14364  rng1zr  14365  rngen1zr0  14367  srgcl  14380  srg1zr  14397  srgen1zr0  14398  ringcl  14423  crngcom  14424  ringidss  14440  mulgass2  14469  imasring  14477  opprmulg  14484  unitmulclb  14529  unitdvcl  14551  rhmmul  14579  rhmdvdsr  14590  subrngmcl  14625  subrgmcl  14649  subrgdv  14654  subrgugrp  14656  domneq0  14689  scafvalg  14752  lmodprop2d  14793  lssclg  14809  lssvnegcl  14821  lssintclm  14829  sralmod  14895  rnglidlmcl  14925  lidlnegcl  14930  rspssp  14939  rnglidlmsgrp  14942  rnglidlrng  14943  2idlcpblrng  14968  qus2idrng  14970  zndvds  15092  znleval2  15097  assa2ass  15117  assa2ass2  15118  asclmul1  15137  asclmul2  15138  ascldimul  15139  asclmulg  15152  psrbagdceq  15167  psrbaglesupp  15171  psrbaglecl  15172  psrbagaddclfi  15173  psrbagcon  15174  psrringfi  15213  mvrf1fi  15219  basgen  15323  2basgeng  15325  iuncld  15358  neipsm  15397  opnneissb  15398  opnssneib  15399  iscnp3  15446  cnprcl2k  15449  cnpnei  15462  cncnp2m  15474  cnptoprest  15482  sslm  15490  upxp  15515  cnmpt22  15537  distspace  15578  0met  15627  blvalps  15631  blval  15632  ssblps  15668  ssbl  15669  blpnfctr  15682  blopn  15733  blnei  15735  bdxmet  15744  bdbl  15746  metcnp3  15754  tgqioo  15798  ptolemy  16068  sinq12gt0  16074  sincosq1eq  16083  rpcxpadd  16155  cxpmul  16162  rplogbval  16198  logbleb  16214  logbgcd1irr  16220  logbprmirr  16225  pellexlem1  16246  chtqwordi  16280  efchtqdvds  16282  ppiqwordi  16285  bcmono  16321  lgsfvalg  16346  lgsneg1  16366  lgssq  16381  lgsdinn0  16389  gausslemma2dlem1a  16399  2lgs  16445  2lgsoddprmlem2  16447  funvtxdm2domval  16492  funiedgdm2domval  16493  iedgedgg  16524  lpvtx  16542  incistruhgr  16553  ausgrumgrien  16633  ausgrusgrien  16634  umgr2edgneu  16675  ushgredgedg  16689  ushgredgedgloop  16691  usgr2v1e2w  16709  egrsubgr  16726  subumgredg2en  16734  iswlk  16786  wlkl1loop  16821  uspgr2wlkeq  16828  istrl  16848  clwwlkccatlem  16863  clwwlkccat  16864  clwwlknccat  16886  clwwlknonex2lem2  16901  clwwlknonex2  16902  iseupth  16910  eupth2lem3lem6fi  16934  konigsbergssiedgwen  16949  bdfind  17194  repiecele0  17298  repiecege0  17299