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

Theorem 3impib 1281
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impib.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
3impib ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impib
StepHypRef Expression
1 3impib.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expd 451 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1275 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  mob  3421  eqreu  3431  dedth3h  4174  prproe  4466  rbropap  5045  breldmg  5362  ssimaexg  6303  funopdmsn  6455  wfr3g  7458  dfsmo2  7489  omwordri  7697  3ecoptocl  7882  cfslb  9126  cofsmo  9129  cfsmolem  9130  coftr  9133  domtriomlem  9302  zorn2lem7  9362  ttukey2g  9376  gchi  9484  tskxpss  9632  tskord  9640  infm3  11020  uzind  11507  fzind  11513  fnn0ind  11514  xltnegi  12085  axdc4uz  12823  facwordi  13116  swrdnd2  13479  cshwidxmod  13595  relexpsucr  13813  relexpsucl  13817  relexprelg  13822  relexpaddnn  13835  caubnd  14142  mulgcd  15312  lcmfdvds  15402  lcmfdvdsb  15403  coprmdvds1  15412  pcfac  15650  ramz  15776  imasleval  16248  cictr  16512  initoeu2lem1  16711  drsdir  16982  psasym  17257  pstr  17258  tsrlin  17266  dirge  17284  mgmcl  17292  mhmlin  17389  mhmmulg  17630  issubg2  17656  nsgbi  17672  cygabl  18338  gsumcom2  18420  srgmulgass  18577  dvdsrtr  18698  drnginvrcl  18812  drnginvrn0  18813  drnginvrl  18814  drnginvrr  18815  isdrngd  18820  issubrg2  18848  abvmul  18877  abvtri  18878  lmhmlin  19083  domnmuln0  19346  ipcj  20027  cssincl  20080  obsip  20113  decpmatmulsumfsupp  20626  mp2pm2mplem4  20662  pm2mpghm  20669  pm2mpmhmlem1  20671  inopn  20752  basis1  20802  iscldtop  20947  2ndcdisj  21307  cnmpt2t  21524  cnmpt22  21525  cnmptcom  21529  fbasssin  21687  ptcmplem3  21905  xmeteq0  22190  prdsxmslem2  22381  nmvs  22527  nmolb  22568  volfiniun  23361  sincosq1sgn  24295  sincosq2sgn  24296  sincosq3sgn  24297  sincosq4sgn  24298  ewlkle  26557  wwlksnext  26856  umgr2adedgwlklem  26909  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  umgrwwlks2on  26923  wwlksext2clwwlkOLD  27022  clwlksfclwwlk  27049  conngrv2edg  27173  frgrwopregasn  27296  frgrwopregbsn  27297  frgrwopreglem5  27301  frgrwopreglem5ALT  27302  frgr2wwlkeu  27307  ablocom  27530  nmcvcn  27678  ipassi  27824  htth  27903  shaddcl  28202  shmulcl  28203  shsubcl  28205  chlimi  28219  pjspansn  28564  cnopc  28900  cnfnc  28917  adj1  28920  lnfnmul  29035  atord  29375  atcvat2  29376  cdj3i  29428  nexple  30199  signstfvc  30779  bnj910  31144  bnj1154  31193  pconncn  31332  mrsubccat  31541  shftvalg  31743  frr3g  31904  frrlem5e  31913  linethru  32385  sin2h  33529  cos2h  33530  tan2h  33531  dvasin  33626  areacirclem1  33630  riotasv  34563  lsmsatcv  34615  omllaw  34848  2llnjN  35171  dalawlem10  35484  dalawlem13  35487  dalawlem14  35488  pclfinclN  35554  ismrc  37581  fzsplit1nn0  37634  pell1234qrmulcl  37736  pell14qrmulcl  37744  iunrelexp0  38311  bi23impib  39008  bi13impib  39009  trelded  39098  suctrALT  39375  suctrALTcf  39472  suctrALTcfVD  39473  stoweidlem17  40552  zm1nn  41641  bgoldbtbndlem4  42021  bgoldbtbnd  42022  tgblthelfgott  42028  tgblthelfgottOLD  42034  mgmhmlin  42111  issubmgm2  42115  clcllaw  42152  rnghmmul  42225  ztprmneprm  42450  lcoel0  42542  linindslinci  42562
  Copyright terms: Public domain W3C validator