MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3impa Structured version   Visualization version   GIF version

Theorem 3impa 1107
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1108 by Wolf Lammen, 20-Jun-2022.)
Hypothesis
Ref Expression
3impa.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
3impa ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impa
StepHypRef Expression
1 df-3an 1086 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 3impa.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylbi 216 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084
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 206  df-3an 1086
This theorem is referenced by:  3imp  1108  3adant1  1127  3adant2  1128  ex3  1343  3impdir  1348  syl3an9b  1431  biimp3a  1466  stoic3  1771  rspec3  3268  vtocl3gaf  3562  vtocl3ga  3564  rspc3v  3624  raltpg  4707  rextpg  4708  disjiun  5140  otthg  5491  3optocl  5778  fun2ssres  6604  funtpg  6614  funssfv  6922  f1elima  7278  ot1stg  8017  ot2ndg  8018  smogt  8397  omord2  8597  omword  8600  oeword  8620  omabslem  8680  ecovass  8853  fpmg  8897  findcard  9201  endjudisj  10211  cfsmolem  10313  ingru  10858  addasspi  10938  mulasspi  10940  ltapi  10946  ltmpi  10947  axpre-ltadd  11210  leltne  11353  dedekind  11427  recextlem2  11895  divdiv32  11973  divdiv1  11976  lble  12218  fnn0ind  12713  supminf  12971  xrleltne  13178  xrmaxeq  13212  xrmineq  13213  iccgelb  13434  elicc4  13445  iccsplit  13516  elfz  13544  modabs  13924  expgt0  14115  expge0  14118  expge1  14119  mulexpz  14122  expp1z  14131  expm1  14132  expmordi  14186  digit1  14254  faclbnd4  14314  faclbnd5  14315  ccatsymb  14590  s3eqs2s1eq  14947  abssubne0  15321  binom  15834  dvds0lem  16269  dvdsnegb  16276  muldvds1  16283  muldvds2  16284  dvdscmulr  16287  dvdsmulcr  16288  divalgmodcl  16409  gcd2n0cl  16509  gcdaddm  16525  lcmdvds  16609  prmdvdsexp  16716  rpexp1i  16725  monpropd  17753  prfval  18223  xpcpropd  18233  curf2ndf  18272  eqglact  19173  ghmqusker  19281  mndodcongi  19541  oddvdsnn0  19542  efgi0  19718  efgi1  19719  efgsval2  19731  lss0cl  20924  mpofrlmd  21775  evls1fpws  22360  scmatscmid  22499  pmatcollpw3fi1lem1  22779  cnpval  23231  cnf2  23244  cnnei  23277  lfinun  23520  ptpjcn  23606  cnmptk2  23681  flfval  23985  cnmpt2plusg  24083  cnmpt2vsca  24190  ustincl  24203  xbln0  24411  blssec  24432  blpnfctr  24433  mopni2  24493  mopni3  24494  nmoval  24723  nmocl  24728  isnghm2  24732  isnmhm2  24760  cnmpt2ds  24850  metdseq0  24861  cnmpt2ip  25267  caucfil  25302  mbfimasn  25652  dvnf  25948  dvnbss  25949  coemul  26279  dvply1  26311  dvnply2  26315  pserdvlem2  26458  logeftb  26610  advlogexp  26682  cxpne0  26704  cxpp1  26707  elno2  27684  f1otrg  28798  ax5seglem9  28871  uhgrn0  29003  upgrn0  29025  upgrle  29026  uhgrwkspthlem2  29691  frgrhash2wsp  30265  sspval  30656  sspnval  30670  lnof  30688  nmooval  30696  nmooge0  30700  nmoub3i  30706  bloln  30717  nmblore  30719  hosval  31673  homval  31674  hodval  31675  hfsval  31676  hfmval  31677  homulass  31735  hoadddir  31737  nmopub2tALT  31842  nmfnleub2  31859  kbval  31887  lnopmul  31900  0lnfn  31918  lnopcoi  31936  nmcoplb  31963  nmcfnlb  31987  kbass2  32050  nmopleid  32072  hstoh  32165  mdi  32228  dmdi  32235  dmdi4  32240  fdifsuppconst  32601  supxrnemnf  32672  rloccring  33125  reofld  33219  nsgmgclem  33286  rhmimaidl  33307  dfufd2lem  33424  r1plmhm  33477  r1pquslmic  33478  lbsdiflsp0  33521  evls1fldgencl  33556  zarclsun  33685  zarclsint  33687  bnj605  34752  bnj607  34761  bnj1097  34826  fnrelpredd  34926  cusgredgex  34949  topdifinffinlem  37054  lindsdom  37315  lindsenlbs  37316  ftc1anclem2  37395  fzmul  37442  nninfnub  37452  exidreslem  37578  grposnOLD  37583  ghomf  37591  rngohomf  37667  rngohom1  37669  rngohomadd  37670  rngohommul  37671  rngoiso1o  37680  rngoisohom  37681  igenmin  37765  lkrcl  38790  lkrf0  38791  omlfh1N  38956  tendoex  40674  uzindd  41675  primrootsunit1  41795  sticksstones3  41846  sticksstones10  41853  sticksstones12a  41855  sticksstones12  41856  sticksstones17  41861  3anrabdioph  42439  3orrabdioph  42440  rencldnfilem  42477  dvdsabsmod0  42645  jm2.18  42646  jm2.25  42657  jm2.15nn0  42661  tfsconcatlem  43002  onsucunitp  43039  addrfv  44143  subrfv  44144  mulvfv  44145  bi3impa  44160  ssfiunibd  44924  supminfxr  45079  limsupgtlem  45398  xlimmnfv  45455  xlimpnfv  45459  dvnmul  45564  stoweidlem34  45655  stoweidlem48  45669  sge0cl  46002  sge0xp  46050  ovnsubaddlem1  46191  aovmpt4g  46814  gboge9  47336
  Copyright terms: Public domain W3C validator