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  12526  fzind  12532  fnn0ind  12533  xltnegi  13064  axdc4uz  13818  facwordi  14117  swrdnd2  14475  cshwidxmod  14623  relexpsucl  14850  relexpsucr  14851  relexprelg  14857  relexpaddnn  14870  caubnd  15178  mulgcd  16364  lcmfdvds  16453  lcmfdvdsb  16454  coprmdvds1  16463  pcfac  16706  ramz  16832  imasleval  17358  cictr  17623  initoeu2lem1  17835  drsdir  18126  psasym  18400  pstr  18401  tsrlin  18409  dirge  18427  mgmcl  18435  mhmlin  18544  mhmmulg  18850  issubg2  18876  nsgbi  18892  gsumcom2  19682  srgmulgass  19873  dvdsrtr  20005  drnginvrcl  20129  drnginvrn0  20130  drnginvrl  20132  drnginvrr  20133  isdrngd  20138  issubrg2  20166  abvmul  20212  abvtri  20213  lmhmlin  20420  domnmuln0  20692  ipcj  20962  cssincl  21016  obsip  21051  decpmatmulsumfsupp  22045  mp2pm2mplem4  22081  pm2mpghm  22088  pm2mpmhmlem1  22090  inopn  22171  basis1  22223  iscldtop  22369  2ndcdisj  22730  cnmpt2t  22947  cnmpt22  22948  cnmptcom  22952  fbasssin  23110  ptcmplem3  23328  xmeteq0  23614  prdsxmslem2  23808  nmvs  23963  nmolb  24004  volfiniun  24834  sincosq1sgn  25778  sincosq2sgn  25779  sincosq3sgn  25780  sincosq4sgn  25781  ewlkle  28352  wwlksnext  28637  umgr2adedgwlklem  28688  elwwlks2ons3im  28698  umgrwwlks2on  28701  conngrv2edg  28938  frgrwopregasn  29059  frgrwopregbsn  29060  frgrwopreglem5  29064  frgrwopreglem5ALT  29065  frgr2wwlkeu  29070  ablocom  29289  nmcvcn  29436  ipassi  29582  htth  29659  shaddcl  29958  shmulcl  29959  shsubcl  29961  chlimi  29975  pjspansn  30318  cnopc  30654  cnfnc  30671  adj1  30674  lnfnmul  30789  atord  31129  atcvat2  31130  cdj3i  31182  nexple  32382  signstfvc  32960  bnj910  33334  bnj1154  33385  umgr2cycllem  33508  pconncn  33592  mrsubccat  33886  shftvalg  34095  addsproplem2  34273  negsproplem2  34310  linethru  34634  sin2h  35964  cos2h  35965  tan2h  35966  dvasin  36058  areacirclem1  36062  riotasv  37317  lsmsatcv  37368  omllaw  37601  2llnjN  37926  dalawlem10  38239  dalawlem13  38242  dalawlem14  38243  pclfinclN  38309  ismrc  40890  fzsplit1nn0  40943  pell1234qrmulcl  41044  pell14qrmulcl  41052  iunrelexp0  41737  bi23impib  42532  bi13impib  42533  trelded  42612  suctrALT  42873  suctrALTcf  42969  suctrALTcfVD  42970  stoweidlem17  44013  zm1nn  45289  bgoldbtbndlem4  45755  bgoldbtbnd  45756  tgblthelfgott  45762  mgmhmlin  45835  issubmgm2  45839  clcllaw  45880  rnghmmul  45953  ztprmneprm  46178  lcoel0  46264  linindslinci  46284  fv2arycl  46489
  Copyright terms: Public domain W3C validator