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

Theorem 3impib 1117
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 417 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1112 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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-an 398  df-3an 1090
This theorem is referenced by:  3impia  1118  mob  3674  eqreu  3686  dedth3h  4545  prproe  4862  rbropap  5520  breldmg  5862  ssimaexg  6923  funopdmsn  7091  fpr3g  8184  wfr3g  8221  dfsmo2  8261  omwordri  8487  3ecoptocl  8682  ttrclselem2  9596  frr3g  9626  cfslb  10136  cofsmo  10139  cfsmolem  10140  coftr  10143  domtriomlem  10312  zorn2lem7  10372  ttukey2g  10386  gchi  10494  tskxpss  10642  tskord  10650  infm3  12048  uzind  12529  fzind  12535  fnn0ind  12536  xltnegi  13065  axdc4uz  13819  facwordi  14118  swrdnd2  14476  cshwidxmod  14624  relexpsucl  14851  relexpsucr  14852  relexprelg  14858  relexpaddnn  14871  caubnd  15179  mulgcd  16365  lcmfdvds  16454  lcmfdvdsb  16455  coprmdvds1  16464  pcfac  16707  ramz  16833  imasleval  17359  cictr  17624  initoeu2lem1  17836  drsdir  18127  psasym  18401  pstr  18402  tsrlin  18410  dirge  18428  mgmcl  18436  mhmlin  18545  mhmmulg  18852  issubg2  18878  nsgbi  18894  gsumcom2  19687  srgmulgass  19878  dvdsrtr  20010  drnginvrcl  20134  drnginvrn0  20135  drnginvrl  20137  drnginvrr  20138  isdrngd  20143  issubrg2  20171  abvmul  20217  abvtri  20218  lmhmlin  20425  domnmuln0  20697  ipcj  20967  cssincl  21021  obsip  21056  decpmatmulsumfsupp  22050  mp2pm2mplem4  22086  pm2mpghm  22093  pm2mpmhmlem1  22095  inopn  22176  basis1  22228  iscldtop  22374  2ndcdisj  22735  cnmpt2t  22952  cnmpt22  22953  cnmptcom  22957  fbasssin  23115  ptcmplem3  23333  xmeteq0  23619  prdsxmslem2  23813  nmvs  23968  nmolb  24009  volfiniun  24839  sincosq1sgn  25783  sincosq2sgn  25784  sincosq3sgn  25785  sincosq4sgn  25786  ewlkle  28358  wwlksnext  28643  umgr2adedgwlklem  28694  elwwlks2ons3im  28704  umgrwwlks2on  28707  conngrv2edg  28944  frgrwopregasn  29065  frgrwopregbsn  29066  frgrwopreglem5  29070  frgrwopreglem5ALT  29071  frgr2wwlkeu  29076  ablocom  29295  nmcvcn  29442  ipassi  29588  htth  29665  shaddcl  29964  shmulcl  29965  shsubcl  29967  chlimi  29981  pjspansn  30324  cnopc  30660  cnfnc  30677  adj1  30680  lnfnmul  30795  atord  31135  atcvat2  31136  cdj3i  31188  nexple  32388  signstfvc  32966  bnj910  33340  bnj1154  33391  umgr2cycllem  33514  pconncn  33598  mrsubccat  33892  shftvalg  34098  addsproplem2  34278  negsproplem2  34315  negsid  34327  linethru  34669  sin2h  35999  cos2h  36000  tan2h  36001  dvasin  36093  areacirclem1  36097  riotasv  37352  lsmsatcv  37403  omllaw  37636  2llnjN  37961  dalawlem10  38274  dalawlem13  38277  dalawlem14  38278  pclfinclN  38344  ismrc  40926  fzsplit1nn0  40979  pell1234qrmulcl  41080  pell14qrmulcl  41088  iunrelexp0  41773  bi23impib  42568  bi13impib  42569  trelded  42648  suctrALT  42909  suctrALTcf  43005  suctrALTcfVD  43006  stoweidlem17  44049  zm1nn  45325  bgoldbtbndlem4  45791  bgoldbtbnd  45792  tgblthelfgott  45798  mgmhmlin  45871  issubmgm2  45875  clcllaw  45916  rnghmmul  45989  ztprmneprm  46214  lcoel0  46300  linindslinci  46320  fv2arycl  46525
  Copyright terms: Public domain W3C validator