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

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 419	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1108	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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  3656  eqreu  3668  dedth3h  4483  prproe  4798  rbropap  5415  breldmg  5742  ssimaexg  6724  funopdmsn  6889  wfr3g  7936  dfsmo2  7967  omwordri  8181  3ecoptocl  8372  cfslb  9677  cofsmo  9680  cfsmolem  9681  coftr  9684  domtriomlem  9853  zorn2lem7  9913  ttukey2g  9927  gchi  10035  tskxpss  10183  tskord  10191  infm3  11587  uzind  12062  fzind  12068  fnn0ind  12069  xltnegi  12597  axdc4uz  13347  facwordi  13645  swrdnd2  14008  cshwidxmod  14156  relexpsucl  14382  relexpsucr  14383  relexprelg  14389  relexpaddnn  14402  caubnd  14710  mulgcd  15886  lcmfdvds  15976  lcmfdvdsb  15977  coprmdvds1  15986  pcfac  16225  ramz  16351  imasleval  16806  cictr  17067  initoeu2lem1  17266  drsdir  17537  psasym  17812  pstr  17813  tsrlin  17821  dirge  17839  mgmcl  17847  mhmlin  17955  mhmmulg  18260  issubg2  18286  nsgbi  18301  cygablOLD  19004  gsumcom2  19088  srgmulgass  19274  dvdsrtr  19398  drnginvrcl  19512  drnginvrn0  19513  drnginvrl  19514  drnginvrr  19515  isdrngd  19520  issubrg2  19548  abvmul  19593  abvtri  19594  lmhmlin  19800  domnmuln0  20064  ipcj  20323  cssincl  20377  obsip  20410  decpmatmulsumfsupp  21378  mp2pm2mplem4  21414  pm2mpghm  21421  pm2mpmhmlem1  21423  inopn  21504  basis1  21555  iscldtop  21700  2ndcdisj  22061  cnmpt2t  22278  cnmpt22  22279  cnmptcom  22283  fbasssin  22441  ptcmplem3  22659  xmeteq0  22945  prdsxmslem2  23136  nmvs  23282  nmolb  23323  volfiniun  24151  sincosq1sgn  25091  sincosq2sgn  25092  sincosq3sgn  25093  sincosq4sgn  25094  ewlkle  27395  wwlksnext  27679  umgr2adedgwlklem  27730  elwwlks2ons3im  27740  umgrwwlks2on  27743  conngrv2edg  27980  frgrwopregasn  28101  frgrwopregbsn  28102  frgrwopreglem5  28106  frgrwopreglem5ALT  28107  frgr2wwlkeu  28112  ablocom  28331  nmcvcn  28478  ipassi  28624  htth  28701  shaddcl  29000  shmulcl  29001  shsubcl  29003  chlimi  29017  pjspansn  29360  cnopc  29696  cnfnc  29713  adj1  29716  lnfnmul  29831  atord  30171  atcvat2  30172  cdj3i  30224  nexple  31378  signstfvc  31954  bnj910  32330  bnj1154  32381  umgr2cycllem  32500  pconncn  32584  mrsubccat  32878  shftvalg  33076  frr3g  33234  fpr3g  33235  linethru  33727  sin2h  35047  cos2h  35048  tan2h  35049  dvasin  35141  areacirclem1  35145  riotasv  36255  lsmsatcv  36306  omllaw  36539  2llnjN  36863  dalawlem10  37176  dalawlem13  37179  dalawlem14  37180  pclfinclN  37246  ismrc  39642  fzsplit1nn0  39695  pell1234qrmulcl  39796  pell14qrmulcl  39804  iunrelexp0  40403  bi23impib  41191  bi13impib  41192  trelded  41271  suctrALT  41532  suctrALTcf  41628  suctrALTcfVD  41629  stoweidlem17  42659  zm1nn  43859  bgoldbtbndlem4  44326  bgoldbtbnd  44327  tgblthelfgott  44333  mgmhmlin  44406  issubmgm2  44410  clcllaw  44451  rnghmmul  44524  ztprmneprm  44749  lcoel0  44837  linindslinci  44857  fv2arycl  45062