Theorem 3ad2ant1 1044

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simp1l  1047  simp1r  1048  simp11  1053  simp12  1054  simp13  1055  simp1ll  1086  simp1lr  1087  simp1rl  1088  simp1rr  1089  simp1l1  1116  simp1l2  1117  simp1l3  1118  simp1r1  1119  simp1r2  1120  simp1r3  1121  simp11l  1134  simp11r  1135  simp12l  1136  simp12r  1137  simp13l  1138  simp13r  1139  simp111  1152  simp112  1153  simp113  1154  simp121  1155  simp122  1156  simp123  1157  simp131  1158  simp132  1159  simp133  1160  3anim123i  1210  3jaao  1344  ceqsalt  2829  sbciegft  3062  reupick2  3493  ifbothdc  3640  frirrg  4447  breldmg  4937  fntpg  5386  funimaexglem  5413  fex2  5503  fvun1  5712  fprg  5837  fsnunfv  5855  fnfvima  5889  cocan1  5928  cocan2  5929  mpoeq3dv  6087  fovcld  6126  fvmpopr2d  6158  funexw  6274  mpofvex  6370  poxp  6397  smoiso  6468  tfrlem5  6480  tfrlemibxssdm  6493  tfr1onlembfn  6510  tfri1dALT  6517  tfrcllembfn  6523  rdgon  6552  freccllem  6568  nnawordex  6697  1dom1el  6993  mapxpen  7034  fidceq  7056  fidifsnen  7057  dif1en  7068  en2eqpr  7099  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  fisseneq  7127  ordiso2  7234  updjud  7281  mkvprop  7357  endjudisj  7425  xpdjuen  7433  mulcanenq0ec  7665  prltlu  7707  prarloclem3step  7716  prarloclem5  7720  ltasrg  7990  cnegexlem1  8354  addcan  8359  apcotr  8787  apadd1  8788  mulext1  8792  divdivap1  8903  divdivap2  8904  div2negap  8915  divneg2ap  8916  ltmulgt11  9044  ltdiv2  9067  squeeze0  9084  nndivtr  9185  nn0n0n1ge2  9550  zdivmul  9570  gtndiv  9575  eluzuzle  9764  eluzp1p1  9782  qdivcl  9877  irrmul  9881  rpgecl  9917  xaddass  10104  xltadd1  10111  xlt2add  10115  lbico1  10165  lbicc2  10219  zltaddlt1le  10242  uzsubsubfz  10282  elfz1b  10325  elfz0ubfz0  10360  fz0fzelfz0  10362  difelfzle  10369  difelfznle  10370  2ffzeq  10376  fzo1fzo0n0  10423  ubmelfzo  10446  fzonn0p1p1  10459  elfzom1p1elfzo  10460  elfzonelfzo  10476  subfzo0  10489  ceiqle  10576  ceilqle  10577  modqval  10587  flqpmodeq  10590  modq0  10592  negqmod0  10594  modqge0  10595  modqlt  10596  modqdiffl  10598  modqmulnn  10605  modqvalp1  10606  modqmuladdnn0  10631  qnegmod  10632  addmodid  10635  modfzo0difsn  10658  addmodlteq  10661  qexpclz  10823  expgt1  10840  expp1zap  10851  expm1ap  10852  expubnd  10859  bernneq2  10924  expnlbnd  10927  mulsubdivbinom2ap  10974  omgadd  11066  hashun  11069  fihashssdif  11083  hashdifpr  11085  fimaxq  11092  ccatval2  11179  ccatval3  11180  ccatval1lsw  11185  ccatval21sw  11186  ccatass  11189  ccatw2s1leng  11219  ccats1val2  11221  ccat2s1fvwd  11228  fzowrddc  11232  swrdval  11233  swrdclg  11235  swrdval2  11236  swrdnd  11244  swrdlen2  11247  swrdfv2  11248  ccatswrd  11255  pfxn0  11273  pfxsuff1eqwrdeq  11284  swrdswrdlem  11289  ccats1pfxeq  11299  ccats1pfxeqrex  11300  ccatopth2  11302  wrd2ind  11308  pfxccatin12lem3  11317  pfxccat3  11319  swrdccat  11320  pfxccatpfx2  11322  pfxccat3a  11323  swrdccat3b  11325  pfxccatid  11326  ccats1pfxeqbi  11327  shftuz  11382  mulreap  11429  redivap  11439  imdivap  11446  resqrtcl  11594  xrmaxltsup  11823  xrmaxaddlem  11825  xrmaxadd  11826  xrlemininf  11836  xrminltinf  11837  climuni  11858  addcn2  11875  mulcn2  11877  efsub  12247  sin02gt0  12330  cos12dec  12334  dvdsval2  12356  addmodlteqALT  12425  modremain  12495  fldivndvdslt  12503  mulgcdr  12594  gcddiv  12595  rpmulgcd  12602  rplpwr  12603  rppwr  12604  nnminle  12611  qredeq  12673  divgcdcoprmex  12679  cncongr1  12680  cncongr2  12681  dvdsnprmd  12702  euclemma  12723  prmexpb  12728  qnumdenbi  12769  eulerth  12810  fermltl  12811  prmdiv  12812  hashgcdlem  12815  odzcllem  12820  vfermltl  12829  reumodprminv  12831  modprm0  12832  modprmn0modprm0  12834  coprimeprodsq  12835  pythagtriplem1  12843  pythagtriplem3  12845  pythagtriplem4  12846  pythagtriplem10  12847  pythagtriplem6  12848  pythagtriplem7  12849  pythagtriplem8  12850  pythagtriplem9  12851  pythagtriplem11  12852  pythagtriplem12  12853  pythagtriplem13  12854  pythagtriplem14  12855  pythagtriplem15  12856  pythagtriplem16  12857  pythagtriplem17  12858  pythagtriplem19  12860  pythagtrip  12861  pcpremul  12871  pcdvdsb  12898  dvdsprmpweqnn  12914  dvdsprmpweqle  12915  difsqpwdvds  12916  pcfaclem  12927  pcbc  12929  4sqlem12  12980  unennn  13023  nninfdc  13079  setsex  13119  f1ocpbllem  13398  imasaddfnlemg  13402  imasaddvallemg  13403  ercpbl  13419  erlecpbl  13420  qusaddvallemg  13421  fvprif  13431  xpsfrnel2  13434  plusfvalg  13451  imasmnd  13541  insubm  13573  grpidrcan  13653  grpidlcan  13654  grpsubpropd2  13693  pwsinvg  13700  imasgrp2  13702  imasgrp  13703  mulgnnsubcl  13726  mulgnn0subcl  13727  mulgsubcl  13728  mulgaddcom  13738  mulginvcom  13739  mulgnnass  13749  mulgassr  13752  mulgpropdg  13756  submmulg  13758  subgcl  13776  subgsubcl  13777  subgsub  13778  subgmulg  13780  nsgconj  13798  ghmsub  13843  ghmrn  13849  ghmeqker  13863  f1ghm0to0  13864  ablinvadd  13902  ablsub4  13905  abladdsub4  13906  subcmnd  13925  imasabl  13928  rngcl  13963  imasrng  13975  srgcl  13989  srg1zr  14006  srgen1zr  14007  ringcl  14032  crngcom  14033  ringidss  14048  mulgass2  14077  imasring  14083  opprmulg  14090  unitmulclb  14134  unitdvcl  14156  rhmmul  14184  rhmdvdsr  14195  subrngmcl  14229  subrgmcl  14253  subrgdv  14258  subrgugrp  14260  domneq0  14292  scafvalg  14327  lmodprop2d  14368  lssclg  14384  lssvnegcl  14396  lssintclm  14404  sralmod  14470  rnglidlmcl  14500  lidlnegcl  14505  rspssp  14514  rnglidlmsgrp  14517  rnglidlrng  14518  2idlcpblrng  14543  qus2idrng  14545  zndvds  14669  znleval2  14674  basgen  14810  2basgeng  14812  iuncld  14845  neipsm  14884  opnneissb  14885  opnssneib  14886  iscnp3  14933  cnprcl2k  14936  cnpnei  14949  cncnp2m  14961  cnptoprest  14969  sslm  14977  upxp  15002  cnmpt22  15024  distspace  15065  0met  15114  blvalps  15118  blval  15119  ssblps  15155  ssbl  15156  blpnfctr  15169  blopn  15220  blnei  15222  bdxmet  15231  bdbl  15233  metcnp3  15241  tgqioo  15285  ptolemy  15554  sinq12gt0  15560  sincosq1eq  15569  rpcxpadd  15635  cxpmul  15642  rplogbval  15675  logbleb  15691  logbgcd1irr  15697  logbprmirr  15702  lgsfvalg  15740  lgsneg1  15760  lgssq  15775  lgsdinn0  15783  gausslemma2dlem1a  15793  2lgs  15839  2lgsoddprmlem2  15841  funvtxdm2domval  15886  funiedgdm2domval  15887  iedgedgg  15918  lpvtx  15936  incistruhgr  15947  ausgrumgrien  16027  ausgrusgrien  16028  umgr2edgneu  16069  ushgredgedg  16083  ushgredgedgloop  16085  usgr2v1e2w  16103  egrsubgr  16120  subumgredg2en  16128  iswlk  16180  wlkl1loop  16215  uspgr2wlkeq  16222  istrl  16242  clwwlkccatlem  16257  clwwlkccat  16258  clwwlknccat  16280  clwwlknonex2lem2  16295  clwwlknonex2  16296  iseupth  16304  eupth2lem3lem6fi  16328  bdfind  16567