Theorem 3impa 1109

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1110 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 1088	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3impa.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 217	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-3an 1088

This theorem is referenced by:  3imp  1110  3adant1  1129  3adant2  1130  ex3  1345  3impdir  1350  syl3an9b  1433  biimp3a  1468  stoic3  1772  rspec3  3277  vtocl3gaf  3580  vtocl3ga  3582  rspc3v  3637  raltpg  4702  rextpg  4703  disjiun  5135  otthg  5495  3optocl  5784  fun2ssres  6612  funtpg  6622  funssfv  6927  f1elima  7282  ot1stg  8026  ot2ndg  8027  smogt  8405  omord2  8603  omword  8606  oeword  8626  omabslem  8686  ecovass  8862  fpmg  8906  findcard  9201  endjudisj  10206  cfsmolem  10307  ingru  10852  addasspi  10932  mulasspi  10934  ltapi  10940  ltmpi  10941  axpre-ltadd  11204  leltne  11347  dedekind  11421  recextlem2  11891  divdiv32  11972  divdiv1  11975  lble  12217  fnn0ind  12714  supminf  12974  xrleltne  13183  xrmaxeq  13217  xrmineq  13218  iccgelb  13439  elicc4  13450  iccsplit  13521  elfz  13549  modabs  13940  expgt0  14132  expge0  14135  expge1  14136  mulexpz  14139  expp1z  14148  expm1  14149  expmordi  14203  digit1  14272  faclbnd4  14332  faclbnd5  14333  ccatsymb  14616  s3eqs2s1eq  14973  abssubne0  15351  binom  15862  dvds0lem  16300  dvdsnegb  16307  muldvds1  16314  muldvds2  16315  dvdscmulr  16318  dvdsmulcr  16319  divalgmodcl  16440  gcd2n0cl  16542  gcdaddm  16558  lcmdvds  16641  prmdvdsexp  16748  rpexp1i  16756  monpropd  17784  prfval  18254  xpcpropd  18264  curf2ndf  18303  eqglact  19209  ghmqusker  19317  mndodcongi  19575  oddvdsnn0  19576  efgi0  19752  efgi1  19753  efgsval2  19765  lss0cl  20962  mpofrlmd  21814  evls1fpws  22388  scmatscmid  22527  pmatcollpw3fi1lem1  22807  cnpval  23259  cnf2  23272  cnnei  23305  lfinun  23548  ptpjcn  23634  cnmptk2  23709  flfval  24013  cnmpt2plusg  24111  cnmpt2vsca  24218  ustincl  24231  xbln0  24439  blssec  24460  blpnfctr  24461  mopni2  24521  mopni3  24522  nmoval  24751  nmocl  24756  isnghm2  24760  isnmhm2  24788  cnmpt2ds  24878  metdseq0  24889  cnmpt2ip  25295  caucfil  25330  mbfimasn  25680  dvnf  25977  dvnbss  25978  coemul  26305  dvply1  26339  dvnply2  26343  pserdvlem2  26486  logeftb  26639  advlogexp  26711  cxpne0  26733  cxpp1  26736  elno2  27713  f1otrg  28893  ax5seglem9  28966  uhgrn0  29098  upgrn0  29120  upgrle  29121  uhgrwkspthlem2  29786  frgrhash2wsp  30360  sspval  30751  sspnval  30765  lnof  30783  nmooval  30791  nmooge0  30795  nmoub3i  30801  bloln  30812  nmblore  30814  hosval  31768  homval  31769  hodval  31770  hfsval  31771  hfmval  31772  homulass  31830  hoadddir  31832  nmopub2tALT  31937  nmfnleub2  31954  kbval  31982  lnopmul  31995  0lnfn  32013  lnopcoi  32031  nmcoplb  32058  nmcfnlb  32082  kbass2  32145  nmopleid  32167  hstoh  32260  mdi  32323  dmdi  32330  dmdi4  32335  fdifsuppconst  32703  supxrnemnf  32778  elrgspnlem2  33232  rloccring  33256  reofld  33351  nsgmgclem  33418  rhmimaidl  33439  dfufd2lem  33556  r1plmhm  33609  r1pquslmic  33610  lbsdiflsp0  33653  evls1fldgencl  33694  zarclsun  33830  zarclsint  33832  bnj605  34899  bnj607  34908  bnj1097  34973  fnrelpredd  35081  cusgredgex  35105  topdifinffinlem  37329  lindsdom  37600  lindsenlbs  37601  ftc1anclem2  37680  fzmul  37727  nninfnub  37737  exidreslem  37863  grposnOLD  37868  ghomf  37876  rngohomf  37952  rngohom1  37954  rngohomadd  37955  rngohommul  37956  rngoiso1o  37965  rngoisohom  37966  igenmin  38050  lkrcl  39073  lkrf0  39074  omlfh1N  39239  tendoex  40957  uzindd  41958  primrootsunit1  42078  sticksstones3  42129  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones17  42144  3anrabdioph  42769  3orrabdioph  42770  rencldnfilem  42807  dvdsabsmod0  42975  jm2.18  42976  jm2.25  42987  jm2.15nn0  42991  tfsconcatlem  43325  onsucunitp  43362  addrfv  44464  subrfv  44465  mulvfv  44466  bi3impa  44481  ssfiunibd  45259  supminfxr  45413  limsupgtlem  45732  xlimmnfv  45789  xlimpnfv  45793  dvnmul  45898  stoweidlem34  45989  stoweidlem48  46003  sge0cl  46336  sge0xp  46384  ovnsubaddlem1  46525  aovmpt4g  47150  gboge9  47688