Theorem 3impa 1129

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1130 by Wolf Lammen, 20-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		df-3an 1102	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3impa.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 208	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-3an 1102

This theorem is referenced by:  3imp  1130  3adant1  1153  3adant2  1154  ex3  1448  3impdir  1453  syl3an9b  1551  biimp3a  1586  stoic3  1856  rspec3  3134  rspc3v  3529  raltpg  4439  rextpg  4440  disjiun  4843  otthg  5156  3optocl  5412  fun2ssres  6154  funtpg  6164  funssfv  6438  f1elima  6753  ot1stg  7421  ot2ndg  7422  smogt  7709  omord2  7893  omword  7896  oeword  7916  omabslem  7972  ecovass  8099  fpmg  8127  findcard  8447  cdaun  9288  cfsmolem  9386  ingru  9931  addasspi  10011  mulasspi  10013  ltapi  10019  ltmpi  10020  axpre-ltadd  10282  leltne  10421  dedekind  10494  recextlem2  10952  divdiv32  11027  divdiv1  11030  lble  11269  fnn0ind  11761  supminf  12013  xrleltne  12213  xrmaxeq  12247  xrmineq  12248  iccgelb  12467  elicc4  12477  iccsplit  12547  elfz  12574  fzrevral  12667  modabs  12946  expgt0  13135  expge0  13138  expge1  13139  mulexpz  13142  expp1z  13151  expm1  13152  digit1  13240  faclbnd4  13323  faclbnd5  13324  s3eqs2s1eq  13926  abssubne0  14298  binom  14803  dvds0lem  15234  dvdsnegb  15241  muldvds1  15248  muldvds2  15249  dvdscmulr  15252  dvdsmulcr  15253  divalgmodcl  15369  gcd2n0cl  15469  gcdaddm  15484  lcmdvds  15559  prmdvdsexp  15663  rpexp1i  15669  monpropd  16620  prfval  17063  xpcpropd  17072  curf2ndf  17111  eqglact  17866  mndodcongi  18182  oddvdsnn0  18183  efgi0  18353  efgi1  18354  lss0cl  19170  mpt2frlmd  20346  scmatscmid  20543  pmatcollpw3fi1lem1  20824  cnpval  21274  cnf2  21287  cnnei  21320  lfinun  21562  ptpjcn  21648  cnmptk2  21723  flfval  22027  cnmpt2plusg  22125  cnmpt2vsca  22231  ustincl  22244  xbln0  22452  blssec  22473  blpnfctr  22474  mopni2  22531  mopni3  22532  nmoval  22752  nmocl  22757  isnghm2  22761  isnmhm2  22789  cnmpt2ds  22879  metdseq0  22890  cnmpt2ip  23279  caucfil  23314  mbfimasn  23635  dvnf  23926  dvnbss  23927  coemul  24244  dvply1  24275  dvnply2  24278  pserdvlem2  24418  logeftb  24566  advlogexp  24637  cxpne0  24659  cxpp1  24662  lgsne0  25296  f1otrg  25987  ax5seglem9  26053  uhgrn0  26198  upgrn0  26220  upgrle  26221  uhgrwkspthlem2  26900  frgrhash2wsp  27529  sspval  27928  sspnval  27942  lnof  27960  nmooval  27968  nmooge0  27972  nmoub3i  27978  bloln  27989  nmblore  27991  hosval  28949  homval  28950  hodval  28951  hfsval  28952  hfmval  28953  homulass  29011  hoadddir  29013  nmopub2tALT  29118  nmfnleub2  29135  kbval  29163  lnopmul  29176  0lnfn  29194  lnopcoi  29212  nmcoplb  29239  nmcfnlb  29263  kbass2  29326  nmopleid  29348  hstoh  29441  mdi  29504  dmdi  29511  dmdi4  29516  supxrnemnf  29883  reofld  30187  bnj605  31321  bnj607  31330  bnj1097  31393  elno2  32149  topdifinffinlem  33529  lindsdom  33734  lindsenlbs  33735  ftc1anclem2  33816  fzmul  33866  nninfnub  33876  exidreslem  34005  grposnOLD  34010  ghomf  34018  rngohomf  34094  rngohom1  34096  rngohomadd  34097  rngohommul  34098  rngoiso1o  34107  rngoisohom  34108  igenmin  34192  lkrcl  34890  lkrf0  34891  omlfh1N  35056  tendoex  36773  3anrabdioph  37865  3orrabdioph  37866  rencldnfilem  37903  expmordi  38030  dvdsabsmod0  38072  jm2.18  38073  jm2.25  38084  jm2.15nn0  38088  addrfv  39188  subrfv  39189  mulvfv  39190  bi3impa  39205  ssfiunibd  40021  supminfxr  40190  limsupgtlem  40506  xlimmnfv  40557  xlimpnfv  40561  dvnmul  40655  stoweidlem34  40747  stoweidlem48  40761  sge0cl  41094  sge0xp  41142  ovnsubaddlem1  41283  ovnovollem3  41371  aovmpt4g  41807  gboge9  42244