Theorem 3impa 1116

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 209  df-3an 1095

This theorem is referenced by:  3imp  1117  3adant1  1137  3adant2  1138  ex3  1354  3impdir  1359  syl3an9b  1443  biimp3a  1478  stoic3  1784  rspec3  3261  vtocl3gaf  3525  vtocl3ga  3526  rspc3v  3578  raltpg  4633  rextpg  4634  disjiun  5063  otthg  5428  3optocl  5718  fun2ssres  6534  funtpg  6544  funssfv  6852  f1elima  7211  ot1stg  7949  ot2ndg  7950  smogt  8301  omord2  8496  omword  8499  oeword  8520  omabslem  8580  ecovass  8765  fpmg  8810  findcard  9092  endjudisj  10086  cfsmolem  10187  ingru  10733  addasspi  10813  mulasspi  10815  ltapi  10821  ltmpi  10822  axpre-ltadd  11085  leltne  11230  dedekind  11304  recextlem2  11776  divdiv32  11858  divdiv1  11861  lble  12103  fnn0ind  12623  supminf  12880  xrleltne  13091  xrmaxeq  13126  xrmineq  13127  iccgelb  13350  elicc4  13361  iccsplit  13433  elfz  13462  modabs  13858  expgt0  14052  expge0  14055  expge1  14056  mulexpz  14059  expp1z  14068  expm1  14069  expmordi  14124  digit1  14194  faclbnd4  14254  faclbnd5  14255  ccatsymb  14540  s3eqs2s1eq  14895  abssubne0  15274  binom  15790  dvds0lem  16230  dvdsnegb  16237  muldvds1  16244  muldvds2  16245  dvdscmulr  16248  dvdsmulcr  16249  divalgmodcl  16371  gcd2n0cl  16473  gcdaddm  16489  lcmdvds  16572  prmdvdsexp  16680  rpexp1i  16688  monpropd  17699  prfval  18160  xpcpropd  18169  curf2ndf  18208  eqglact  19149  ghmqusker  19257  mndodcongi  19513  oddvdsnn0  19514  efgi0  19690  efgi1  19691  efgsval2  19703  lss0cl  20941  mpofrlmd  21756  evls1fpws  22359  scmatscmid  22493  pmatcollpw3fi1lem1  22773  cnpval  23223  cnf2  23236  cnnei  23269  lfinun  23512  ptpjcn  23598  cnmptk2  23673  flfval  23977  cnmpt2plusg  24075  cnmpt2vsca  24182  ustincl  24195  xbln0  24401  blssec  24422  blpnfctr  24423  mopni2  24480  mopni3  24481  nmoval  24702  nmocl  24707  isnghm2  24711  isnmhm2  24739  cnmpt2ds  24831  metdseq0  24842  cnmpt2ip  25237  caucfil  25272  mbfimasn  25621  dvnf  25916  dvnbss  25917  coemul  26239  dvply1  26272  dvnply2  26275  pserdvlem2  26415  logeftb  26569  advlogexp  26641  cxpne0  26663  cxpp1  26666  elno2  27640  f1otrg  28961  ax5seglem9  29028  uhgrn0  29158  upgrn0  29180  upgrle  29181  uhgrwkspthlem2  29844  frgrhash2wsp  30424  sspval  30816  sspnval  30830  lnof  30848  nmooval  30856  nmooge0  30860  nmoub3i  30866  bloln  30877  nmblore  30879  hosval  31833  homval  31834  hodval  31835  hfsval  31836  hfmval  31837  homulass  31895  hoadddir  31897  nmopub2tALT  32002  nmfnleub2  32019  kbval  32047  lnopmul  32060  0lnfn  32078  lnopcoi  32096  nmcoplb  32123  nmcfnlb  32147  kbass2  32210  nmopleid  32232  hstoh  32325  mdi  32388  dmdi  32395  dmdi4  32400  tpssg  32629  fdifsuppconst  32785  supxrnemnf  32864  elrgspnlem2  33328  rloccring  33355  reofld  33430  nsgmgclem  33498  rhmimaidl  33519  dfufd2lem  33644  r1plmhm  33705  r1pquslmic  33706  lbsdiflsp0  33822  evls1fldgencl  33866  zarclsun  34066  zarclsint  34068  bnj605  35104  bnj607  35113  bnj1097  35178  fnrelpredd  35287  rankfilimb  35298  cusgredgex  35365  topdifinffinlem  37724  lindsdom  37996  lindsenlbs  37997  ftc1anclem2  38076  fzmul  38123  nninfnub  38133  exidreslem  38259  grposnOLD  38264  ghomf  38272  rngohomf  38348  rngohom1  38350  rngohomadd  38351  rngohommul  38352  rngoiso1o  38361  rngoisohom  38362  igenmin  38446  lkrcl  39599  lkrf0  39600  omlfh1N  39765  tendoex  41482  uzindd  42478  primrootsunit1  42597  sticksstones3  42648  sticksstones10  42655  sticksstones12a  42657  sticksstones12  42658  sticksstones17  42663  3anrabdioph  43246  3orrabdioph  43247  rencldnfilem  43280  dvdsabsmod0  43447  jm2.18  43448  jm2.25  43459  jm2.15nn0  43463  tfsconcatlem  43796  onsucunitp  43833  addrfv  44927  subrfv  44928  mulvfv  44929  bi3impa  44944  ssfiunibd  45771  supminfxr  45921  limsupgtlem  46234  xlimmnfv  46291  xlimpnfv  46295  dvnmul  46400  stoweidlem34  46491  stoweidlem48  46505  sge0cl  46838  sge0xp  46886  ovnsubaddlem1  47027  aovmpt4g  47678  gboge9  48269