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

Theorem 3impib 1253
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 450 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1248 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  mob  3354  eqreu  3364  dedth3h  4090  rbropap  4930  breldmg  5239  ssimaexg  6159  wfr3g  7277  dfsmo2  7308  omwordri  7516  3ecoptocl  7703  cfslb  8948  cofsmo  8951  cfsmolem  8952  coftr  8955  domtriomlem  9124  zorn2lem7  9184  ttukey2g  9198  gchi  9302  tskxpss  9450  tskord  9458  infm3  10831  uzind  11301  fzind  11307  fnn0ind  11308  xltnegi  11880  axdc4uz  12600  facwordi  12893  swrdnd2  13231  cshwidxmod  13346  relexpsucr  13563  relexpsucl  13567  relexprelg  13572  relexpaddnn  13585  caubnd  13892  mulgcd  15049  lcmfdvds  15139  lcmfdvdsb  15140  coprmdvds1  15149  pcfac  15387  ramz  15513  imasleval  15970  cictr  16234  initoeu2lem1  16433  drsdir  16704  psasym  16979  pstr  16980  tsrlin  16988  dirge  17006  mgmcl  17014  mhmlin  17111  mhmmulg  17352  issubg2  17378  nsgbi  17394  cygabl  18061  gsumcom2  18143  srgmulgass  18300  dvdsrtr  18421  drnginvrcl  18533  drnginvrn0  18534  drnginvrl  18535  drnginvrr  18536  isdrngd  18541  issubrg2  18569  abvmul  18598  abvtri  18599  lmhmlin  18802  domnmuln0  19065  ipcj  19743  cssincl  19793  obsip  19826  decpmatmulsumfsupp  20339  mp2pm2mplem4  20375  pm2mpghm  20382  pm2mpmhmlem1  20384  inopn  20471  basis1  20507  iscldtop  20651  2ndcdisj  21011  cnmpt2t  21228  cnmpt22  21229  cnmptcom  21233  fbasssin  21392  ptcmplem3  21610  xmeteq0  21894  prdsxmslem2  22085  nmvs  22223  nmolb  22263  volfiniun  23039  sincosq1sgn  23971  sincosq2sgn  23972  sincosq3sgn  23973  sincosq4sgn  23974  usg2wlk  25911  wwlknext  26018  wwlkext2clwwlk  26097  cusgraisrusgra  26231  rusgra0edg  26248  numclwwlkovf2ex  26379  ablocom  26555  nmcvcn  26735  ipassi  26886  htth  26965  shaddcl  27264  shmulcl  27265  shsubcl  27267  chlimi  27281  pjspansn  27626  cnopc  27962  cnfnc  27979  adj1  27982  lnfnmul  28097  atord  28437  atcvat2  28438  cdj3i  28490  nexple  29205  signstfvc  29783  bnj910  30078  bnj1154  30127  pconcn  30266  mrsubccat  30475  shftvalg  30676  frr3g  30829  linethru  31236  sin2h  32365  cos2h  32366  tan2h  32367  dvasin  32462  areacirclem1  32466  riotasv  33059  lsmsatcv  33111  omllaw  33344  2llnjN  33667  dalawlem10  33980  dalawlem13  33983  dalawlem14  33984  pclfinclN  34050  ismrc  36078  fzsplit1nn0  36131  pell1234qrmulcl  36233  pell14qrmulcl  36241  iunrelexp0  36809  bi23impib  37508  bi13impib  37509  trelded  37598  suctrALT  37879  suctrALTcf  37976  suctrALTcfVD  37977  stoweidlem17  38707  bgoldbtbndlem4  40022  bgoldbtbnd  40023  tgblthelfgott  40027  tgblthelfgottOLD  40034  zm1nn  40168  ewlkle  40802  wwlksnext  41094  umgr2adedgwlklem  41146  elwwlks2ons3  41154  umgrwwlks2on  41156  wwlksext2clwwlk  41226  clwlksfclwwlk  41264  conngrv2edg  41357  av-numclwwlkovf2ex  41512  mgmhmlin  41571  issubmgm2  41575  clcllaw  41612  rnghmmul  41685  ztprmneprm  41913  lcoel0  42006  linindslinci  42026
  Copyright terms: Public domain W3C validator