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

Theorem 3impib 1113
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 419 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1108 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3impia  1114  mob  3694  eqreu  3706  dedth3h  4508  prproe  4822  rbropap  5437  breldmg  5765  ssimaexg  6740  funopdmsn  6903  wfr3g  7949  dfsmo2  7980  omwordri  8194  3ecoptocl  8385  cfslb  9686  cofsmo  9689  cfsmolem  9690  coftr  9693  domtriomlem  9862  zorn2lem7  9922  ttukey2g  9936  gchi  10044  tskxpss  10192  tskord  10200  infm3  11596  uzind  12071  fzind  12077  fnn0ind  12078  xltnegi  12606  axdc4uz  13356  facwordi  13654  swrdnd2  14017  cshwidxmod  14165  relexpsucr  14388  relexpsucl  14392  relexprelg  14397  relexpaddnn  14410  caubnd  14718  mulgcd  15894  lcmfdvds  15984  lcmfdvdsb  15985  coprmdvds1  15994  pcfac  16233  ramz  16359  imasleval  16814  cictr  17075  initoeu2lem1  17274  drsdir  17545  psasym  17820  pstr  17821  tsrlin  17829  dirge  17847  mgmcl  17855  mhmlin  17963  mhmmulg  18268  issubg2  18294  nsgbi  18309  cygablOLD  19011  gsumcom2  19095  srgmulgass  19281  dvdsrtr  19405  drnginvrcl  19519  drnginvrn0  19520  drnginvrl  19521  drnginvrr  19522  isdrngd  19527  issubrg2  19555  abvmul  19600  abvtri  19601  lmhmlin  19807  domnmuln0  20071  ipcj  20778  cssincl  20832  obsip  20865  decpmatmulsumfsupp  21381  mp2pm2mplem4  21417  pm2mpghm  21424  pm2mpmhmlem1  21426  inopn  21507  basis1  21558  iscldtop  21703  2ndcdisj  22064  cnmpt2t  22281  cnmpt22  22282  cnmptcom  22286  fbasssin  22444  ptcmplem3  22662  xmeteq0  22948  prdsxmslem2  23139  nmvs  23285  nmolb  23326  volfiniun  24154  sincosq1sgn  25094  sincosq2sgn  25095  sincosq3sgn  25096  sincosq4sgn  25097  ewlkle  27398  wwlksnext  27682  umgr2adedgwlklem  27733  elwwlks2ons3im  27743  umgrwwlks2on  27746  conngrv2edg  27983  frgrwopregasn  28104  frgrwopregbsn  28105  frgrwopreglem5  28109  frgrwopreglem5ALT  28110  frgr2wwlkeu  28115  ablocom  28334  nmcvcn  28481  ipassi  28627  htth  28704  shaddcl  29003  shmulcl  29004  shsubcl  29006  chlimi  29020  pjspansn  29363  cnopc  29699  cnfnc  29716  adj1  29719  lnfnmul  29834  atord  30174  atcvat2  30175  cdj3i  30227  nexple  31325  signstfvc  31901  bnj910  32277  bnj1154  32328  umgr2cycllem  32444  pconncn  32528  mrsubccat  32822  shftvalg  33020  frr3g  33178  fpr3g  33179  linethru  33671  sin2h  34992  cos2h  34993  tan2h  34994  dvasin  35086  areacirclem1  35090  riotasv  36200  lsmsatcv  36251  omllaw  36484  2llnjN  36808  dalawlem10  37121  dalawlem13  37124  dalawlem14  37125  pclfinclN  37191  ismrc  39558  fzsplit1nn0  39611  pell1234qrmulcl  39712  pell14qrmulcl  39720  iunrelexp0  40319  bi23impib  41111  bi13impib  41112  trelded  41191  suctrALT  41452  suctrALTcf  41548  suctrALTcfVD  41549  stoweidlem17  42585  zm1nn  43785  bgoldbtbndlem4  44252  bgoldbtbnd  44253  tgblthelfgott  44259  mgmhmlin  44332  issubmgm2  44336  clcllaw  44377  rnghmmul  44450  ztprmneprm  44675  lcoel0  44763  linindslinci  44783  fv2arycl  44988
  Copyright terms: Public domain W3C validator