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  3280  vtocl3gf  3532  vtocl3g  3534  rspc2ev  3589  reuss  4273  frc  5618  trssord  6374  funtp  6590  resdif  6839  f1cdmsn  7283  f1ofvswap  7307  fnotovb  7465  fovcdm  7584  fnovrn  7589  fmpoco  8092  mpof1o2d  8123  smoord  8354  odi  8566  oeoa  8585  oeoe  8587  nndi  8611  ecopovtrn  8820  ecovass  8824  ecovdi  8825  unfi  9165  entrfil  9179  domtrfil  9186  f1imaenfi  9189  suppr  9442  infpr  9475  harval2  10002  fin23lem31  10345  tskuni  10792  addasspi  10904  mulasspi  10906  distrpi  10907  mulcanenq  10969  genpass  11018  distrlem1pr  11034  prlem934  11042  ltapr  11054  le2tri3i  11364  subadd  11484  addsub  11492  subdi  11671  submul2  11678  ltaddsub  11712  leaddsub  11714  divval  11898  diveq0  11906  div12  11918  diveq1  11925  divneg  11930  divdiv2  11951  ltmulgt11  12098  gt0div  12105  ge0div  12106  uzind3  12715  fnn0ind  12720  qdivcl  13020  irrmul  13024  xrlttr  13191  fzen  13595  modcyc  13967  modcyc2  13968  rpexpmord  14232  faclbnd4lem4  14360  ccatval21sw  14651  lswccatn0lsw  14658  ccatpfx  14770  ccatopth  14785  cshweqdifid  14891  lenegsq  15408  moddvds  16353  dvdscmulr  16374  dvdsmulcr  16375  dvds2add  16380  dvds2sub  16381  dvdsleabs  16401  divalg  16493  divalgb  16494  ndvdsadd  16500  gcdcllem3  16591  dvdslegcd  16594  modgcd  16622  absmulgcd  16639  odzval  16883  pcmul  16943  ressid2  17326  ressval2  17327  catcisolem  18199  prf1st  18292  prf2nd  18293  1st2ndprf  18294  curfuncf  18326  curf2ndf  18335  pltval  18418  pospo  18431  lubel  18602  isdlat  18610  submgmcl  18809  prdssgrpd  18835  issubmnd  18866  prdsmndd  18877  submcl  18920  grpinvid1  19115  grpinvid2  19116  mulgp1  19230  ghmlin  19348  ghmsub  19351  odlem2  19666  gexlem2  19709  lsmvalx  19766  efgtval  19850  cmncom  19925  lssvnegcl  21140  islss3  21143  prdslmodd  21153  zntoslem  21769  evlslem2  22295  evlseu  22299  maducoeval2  22862  madutpos  22864  madugsum  22865  madurid  22866  m2cpminvid  22978  pm2mpghm  23041  unopn  23128  ntrss  23280  innei  23350  t1sep2  23594  metustsym  24781  cncfi  25122  rrxds  25621  quotval  26522  abelthlem2  26668  mudivsum  27766  padicabv  27866  nosupfv  27942  nosupres  27943  noinffv  27957  sltssepc  28036  divsval  28454  axsegconlem1  29374  loop1cycl  30623  nsnlplig  30962  nsnlpligALT  30963  grpoinvid1  31009  grpoinvid2  31010  grpodivval  31016  ablo4  31031  ablonncan  31037  nvnpcan  31137  nvmeq0  31139  nvabs  31153  imsdval  31167  ipval  31184  nmorepnf  31249  blo3i  31283  blometi  31284  ipasslem5  31316  hvmulcan  31553  his5  31567  his7  31571  his2sub2  31574  hhssabloilem  31742  hhssnv  31745  fh1  32099  fh2  32100  cm2j  32101  homcl  32227  homco1  32282  homulass  32283  hoadddi  32284  hosubsub2  32293  braadd  32426  bramul  32427  lnopmul  32448  lnopli  32449  lnopaddmuli  32454  lnopsubmuli  32456  lnfnli  32521  lnfnaddmuli  32526  kbass2  32598  mdexchi  32816  xdivval  33364  resvid2  33770  resvval2  33771  fedgmullem2  34140  unitdivcld  34411  bnj229  35393  bnj546  35405  bnj570  35414  rankfilimb  35610  cusgredgex2  35721  cvmlift2lem7  35888  finminlem  36937  ivthALT  36954  topdifinffinlem  38101  lindsadd  38367  exidcl  38626  grposnOLD  38632  rngoneglmul  38693  rngonegrmul  38694  divrngcl  38707  crngocom  38751  crngm4  38753  inidl  38780  xrninxpex  39165  oposlem  40055  hlsuprexch  40254  ldilcnv  40988  ltrnu  40994  tgrpgrplem  41622  tgrpabl  41624  erngdvlem3  41863  erngdvlem3-rN  41871  dvalveclem  41898  dvhfvadd  41964  dvhgrp  41980  dvhlveclem  41981  djhval2  42272  fmpocos  43103  resubadd  43254  diophren  43654  monotoddzzfi  43783  ltrmynn0  43789  ltrmxnn0  43790  lermxnn0  43791  rmyeq  43795  lermy  43796  jm2.21  43835  radcnvrat  45138  dvconstbi  45158  expgrowth  45159  bi3impb  45307  xlimmnfvlem2  46661  xlimpnfvlem2  46665  fnotaovb  48086  tposcurf1  50225  precofvalALT  50294  onetansqsecsq  50687