Theorem 3impb 1114

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 420	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  3adant3  1132  syl3an132  1166  3impdi  1351  rsp2e  3251  vtocl3gf  3525  vtocl3g  3527  rspc2ev  3586  reuss  4276  frc  5584  trssord  6331  funtp  6546  resdif  6792  f1cdmsn  7225  f1ofvswap  7249  fnotovb  7407  fovcdm  7525  fnovrn  7530  fmpoco  8034  smoord  8294  odi  8503  oeoa  8521  oeoe  8523  nndi  8547  ecopovtrn  8753  ecovass  8757  ecovdi  8758  unfi  9091  entrfil  9105  domtrfil  9112  f1imaenfi  9115  suppr  9367  infpr  9400  harval2  9901  fin23lem31  10245  tskuni  10685  addasspi  10797  mulasspi  10799  distrpi  10800  mulcanenq  10862  genpass  10911  distrlem1pr  10927  prlem934  10935  ltapr  10947  le2tri3i  11254  subadd  11374  addsub  11382  subdi  11561  submul2  11568  ltaddsub  11602  leaddsub  11604  divval  11789  diveq0  11797  div12  11809  diveq1  11817  divneg  11824  divdiv2  11844  ltmulgt11  11992  gt0div  11999  ge0div  12000  uzind3  12577  fnn0ind  12582  qdivcl  12874  irrmul  12878  xrlttr  13045  fzen  13448  modcyc  13817  modcyc2  13818  rpexpmord  14082  faclbnd4lem4  14210  ccatval21sw  14500  lswccatn0lsw  14506  ccatpfx  14615  ccatopth  14630  cshweqdifid  14734  lenegsq  15235  moddvds  16181  dvdscmulr  16202  dvdsmulcr  16203  dvds2add  16208  dvds2sub  16209  dvdsleabs  16229  divalg  16321  divalgb  16322  ndvdsadd  16328  gcdcllem3  16419  dvdslegcd  16422  modgcd  16450  absmulgcd  16467  odzval  16710  pcmul  16770  ressid2  17152  ressval2  17153  catcisolem  18025  prf1st  18118  prf2nd  18119  1st2ndprf  18120  curfuncf  18152  curf2ndf  18161  pltval  18244  pospo  18257  lubel  18428  isdlat  18436  submgmcl  18623  prdssgrpd  18649  issubmnd  18677  prdsmndd  18686  submcl  18728  grpinvid1  18912  grpinvid2  18913  mulgp1  19028  ghmlin  19141  ghmsub  19144  odlem2  19459  gexlem2  19502  lsmvalx  19559  efgtval  19643  cmncom  19718  lssvnegcl  20898  islss3  20901  prdslmodd  20911  zntoslem  21502  evlslem2  22025  evlseu  22029  maducoeval2  22575  madutpos  22577  madugsum  22578  madurid  22579  m2cpminvid  22688  pm2mpghm  22751  unopn  22838  ntrss  22990  innei  23060  t1sep2  23304  metustsym  24490  cncfi  24834  rrxds  25340  quotval  26247  abelthlem2  26389  mudivsum  27488  padicabv  27588  nosupfv  27665  nosupres  27666  noinffv  27680  ssltsepc  27754  divsval  28148  axsegconlem1  28916  nsnlplig  30482  nsnlpligALT  30483  grpoinvid1  30529  grpoinvid2  30530  grpodivval  30536  ablo4  30551  ablonncan  30557  nvnpcan  30657  nvmeq0  30659  nvabs  30673  imsdval  30687  ipval  30704  nmorepnf  30769  blo3i  30803  blometi  30804  ipasslem5  30836  hvmulcan  31073  his5  31087  his7  31091  his2sub2  31094  hhssabloilem  31262  hhssnv  31265  fh1  31619  fh2  31620  cm2j  31621  homcl  31747  homco1  31802  homulass  31803  hoadddi  31804  hosubsub2  31813  braadd  31946  bramul  31947  lnopmul  31968  lnopli  31969  lnopaddmuli  31974  lnopsubmuli  31976  lnfnli  32041  lnfnaddmuli  32046  kbass2  32118  mdexchi  32336  xdivval  32928  resvid2  33339  resvval2  33340  fedgmullem2  33715  unitdivcld  33986  bnj229  34968  bnj546  34980  bnj570  34989  rankfilimb  35185  cusgredgex2  35239  loop1cycl  35253  cvmlift2lem7  35425  finminlem  36434  ivthALT  36451  topdifinffinlem  37464  lindsadd  37726  exidcl  37989  grposnOLD  37995  rngoneglmul  38056  rngonegrmul  38057  divrngcl  38070  crngocom  38114  crngm4  38116  inidl  38143  xrninxpex  38514  oposlem  39354  hlsuprexch  39553  ldilcnv  40287  ltrnu  40293  tgrpgrplem  40921  tgrpabl  40923  erngdvlem3  41162  erngdvlem3-rN  41170  dvalveclem  41197  dvhfvadd  41263  dvhgrp  41279  dvhlveclem  41280  djhval2  41571  f1o2d2  42404  fmpocos  42405  resubadd  42549  diophren  42970  monotoddzzfi  43099  ltrmynn0  43105  ltrmxnn0  43106  lermxnn0  43107  rmyeq  43111  lermy  43112  jm2.21  43151  radcnvrat  44471  dvconstbi  44491  expgrowth  44492  bi3impb  44641  xlimmnfvlem2  45993  xlimpnfvlem2  45997  fnotaovb  47360  tposcurf1  49460  precofvalALT  49529  onetansqsecsq  49922