Theorem 3impb 1132

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3impb.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

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

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 426	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1128	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3adant3  1150  syl3an132  1184  3impdi  1369  rsp2e  3284  vtocl3gf  3536  vtocl3g  3538  reuss  4275  cotsexgw  5470  frc  5621  trssord  6405  funtp  6627  resdif  6876  f1cdmsn  7321  f1ofvswap  7345  fnotovb  7503  fovcdm  7623  fnovrn  7628  fmpoco  8142  mpof1o2d  8174  smoord  8411  odi  8625  oeoa  8644  oeoe  8646  nndi  8670  ecopovtrn  8879  ecovass  8883  ecovdi  8884  unfi  9224  entrfil  9238  domtrfil  9245  f1imaenfi  9248  suppr  9501  infpr  9534  harval2  10117  fin23lem31  10460  tskuni  10907  addasspi  11019  mulasspi  11021  distrpi  11022  mulcanenq  11084  genpass  11133  distrlem1pr  11149  prlem934  11157  ltapr  11169  le2tri3i  11479  subadd  11599  addsub  11607  subdi  11788  submul2  11795  ltaddsub  11830  leaddsub  11832  divval  12016  diveq0  12024  div12  12036  diveq1  12043  divneg  12048  divdiv2  12069  ltmulgt11  12216  gt0div  12223  ge0div  12224  uzind3  12833  fnn0ind  12838  qdivcl  13138  irrmul  13142  xrlttr  13309  fzen  13714  modcyc  14086  modcyc2  14087  rpexpmord  14351  faclbnd4lem4  14481  ccatval21sw  14772  lswccatn0lsw  14779  ccatpfx  14892  ccatopth  14907  cshweqdifid  15013  lenegsq  15531  moddvds  16477  dvdscmulr  16498  dvdsmulcr  16499  dvds2add  16504  dvds2sub  16505  dvdsleabs  16525  divalg  16617  divalgb  16618  ndvdsadd  16624  gcdcllem3  16715  dvdslegcd  16718  modgcd  16749  absmulgcd  16766  odzval  17013  pcmul  17073  ressid2  17456  ressval2  17457  catcisolem  18335  prf1st  18428  prf2nd  18429  1st2ndprf  18430  curfuncf  18462  curf2ndf  18471  pltval  18554  pospo  18567  lubel  18738  isdlat  18746  submgmcl  18946  prdssgrpd  18972  issubmnd  19003  prdsmndd  19014  submcl  19057  grpinvid1  19252  grpinvid2  19253  mulgp1  19367  ghmlin  19485  ghmsub  19488  odlem2  19804  gexlem2  19847  lsmvalx  19904  efgtval  19988  cmncom  20063  lssvnegcl  21282  islss3  21285  prdslmodd  21295  zntoslem  21917  evlslem2  22443  evlseu  22447  maducoeval2  23010  madutpos  23012  madugsum  23013  madurid  23014  m2cpminvid  23126  pm2mpghm  23189  unopn  23276  ntrss  23428  innei  23498  t1sep2  23742  metustsym  24929  cncfi  25270  rrxds  25769  quotval  26668  abelthlem2  26816  mudivsum  27914  padicabv  28014  nosupfv  28120  nosupres  28121  noinffv  28135  sltssepc  28214  divsval  28632  axsegconlem1  29552  loop1cycl  30801  nsnlplig  31140  nsnlpligALT  31141  grpoinvid1  31187  grpoinvid2  31188  grpodivval  31194  ablo4  31209  ablonncan  31215  nvnpcan  31315  nvmeq0  31317  nvabs  31331  imsdval  31345  ipval  31362  nmorepnf  31427  blo3i  31461  blometi  31462  ipasslem5  31494  hvmulcan  31731  his5  31745  his7  31749  his2sub2  31752  hhssabloilem  31920  hhssnv  31923  fh1  32277  fh2  32278  cm2j  32279  homcl  32405  homco1  32460  homulass  32461  hoadddi  32462  hosubsub2  32471  braadd  32604  bramul  32605  lnopmul  32626  lnopli  32627  lnopaddmuli  32632  lnopsubmuli  32634  lnfnli  32699  lnfnaddmuli  32704  kbass2  32776  mdexchi  32994  xdivval  33581  resvid2  33995  resvval2  33996  fedgmullem2  34373  unitdivcld  34644  bnj229  35625  bnj546  35637  bnj570  35646  rankfilimb  35853  cusgredgex2  36105  cvmlift2lem7  36282  finminlem  37321  ivthALT  37338  topdifinffinlem  38538  lindsadd  38804  exidcl  39076  grposnOLD  39082  rngoneglmul  39143  rngonegrmul  39144  divrngcl  39157  crngocom  39201  crngm4  39203  inidl  39230  xrninxpex  39615  oposlem  40505  hlsuprexch  40704  ldilcnv  41438  ltrnu  41444  tgrpgrplem  42072  tgrpabl  42074  erngdvlem3  42313  erngdvlem3-rN  42321  dvalveclem  42348  dvhfvadd  42414  dvhgrp  42430  dvhlveclem  42431  djhval2  42722  fmpocos  43554  resubadd  43696  diophren  44086  monotoddzzfi  44215  ltrmynn0  44221  ltrmxnn0  44222  lermxnn0  44223  rmyeq  44227  lermy  44228  jm2.21  44267  radcnvrat  45559  dvconstbi  45579  expgrowth  45580  bi3impb  45727  xlimmnfvlem2  47116  xlimpnfvlem2  47120  fnotaovb  48541  tposcurf1  50752  precofvalALT  50834  onetansqsecsq  51282