Theorem 3impib 1116

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 415	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3impia  1117  mob  3672  eqreu  3684  dedth3h  4535  prproe  4856  rbropap  5506  breldmg  5853  ssimaexg  6914  funopdmsn  7089  fpr3g  8221  wfr3g  8255  dfsmo2  8273  omwordri  8493  3ecoptocl  8739  ttrclselem2  9623  frr3g  9656  cfslb  10164  cofsmo  10167  cfsmolem  10168  coftr  10171  domtriomlem  10340  zorn2lem7  10400  ttukey2g  10414  gchi  10522  tskxpss  10670  tskord  10678  infm3  12088  uzind  12571  fzind  12577  fnn0ind  12578  xltnegi  13117  axdc4uz  13893  facwordi  14198  swrdnd2  14565  cshwidxmod  14712  relexpsucl  14940  relexpsucr  14941  relexprelg  14947  relexpaddnn  14960  caubnd  15268  mulgcd  16461  lcmfdvds  16555  lcmfdvdsb  16556  coprmdvds1  16565  pcfac  16813  ramz  16939  imasleval  17447  cictr  17714  initoeu2lem1  17923  drsdir  18210  psasym  18484  pstr  18485  tsrlin  18493  dirge  18511  mgmcl  18553  mgmhmlin  18609  issubmgm2  18613  mhmlin  18703  mhmmulg  19030  issubg2  19056  nsgbi  19071  gsumcom2  19889  srgmulgass  20137  dvdsrtr  20288  rnghmmul  20369  issubrng2  20475  issubrg2  20509  domnmuln0  20626  drnginvrcl  20670  drnginvrn0  20671  drnginvrl  20673  drnginvrr  20674  isdrngd  20682  isdrngdOLD  20684  abvmul  20738  abvtri  20739  lmhmlin  20971  ipcj  21573  cssincl  21627  obsip  21660  decpmatmulsumfsupp  22689  mp2pm2mplem4  22725  pm2mpghm  22732  pm2mpmhmlem1  22734  inopn  22815  basis1  22866  iscldtop  23011  2ndcdisj  23372  cnmpt2t  23589  cnmpt22  23590  cnmptcom  23594  fbasssin  23752  ptcmplem3  23970  xmeteq0  24254  prdsxmslem2  24445  nmvs  24592  nmolb  24633  volfiniun  25476  sincosq1sgn  26435  sincosq2sgn  26436  sincosq3sgn  26437  sincosq4sgn  26438  addsproplem2  27914  negsproplem2  27972  negsid  27984  mulsproplem9  28064  precsexlem10  28155  uzsind  28330  recut  28399  0reno  28400  ewlkle  29586  wwlksnext  29873  umgr2adedgwlklem  29924  elwwlks2ons3im  29934  usgrwwlks2on  29938  umgrwwlks2on  29939  conngrv2edg  30177  frgrwopregasn  30298  frgrwopregbsn  30299  frgrwopreglem5  30303  frgrwopreglem5ALT  30304  frgr2wwlkeu  30309  ablocom  30530  nmcvcn  30677  ipassi  30823  htth  30900  shaddcl  31199  shmulcl  31200  shsubcl  31202  chlimi  31216  pjspansn  31559  cnopc  31895  cnfnc  31912  adj1  31915  lnfnmul  32030  atord  32370  atcvat2  32371  cdj3i  32423  nexple  32832  signstfvc  34608  bnj910  34981  bnj1154  35032  r1filimi  35135  umgr2cycllem  35205  pconncn  35289  mrsubccat  35583  shftvalg  35797  linethru  36218  sin2h  37670  cos2h  37671  tan2h  37672  dvasin  37764  areacirclem1  37768  riotasv  39078  lsmsatcv  39129  omllaw  39362  2llnjN  39686  dalawlem10  39999  dalawlem13  40002  dalawlem14  40003  pclfinclN  40069  ismrc  42818  fzsplit1nn0  42871  pell1234qrmulcl  42972  pell14qrmulcl  42980  onsucf1olem  43387  iunrelexp0  43819  bi23impib  44603  bi13impib  44604  trelded  44682  suctrALT  44942  suctrALTcf  45038  suctrALTcfVD  45039  stoweidlem17  46139  zm1nn  47426  bgoldbtbndlem4  47932  bgoldbtbnd  47933  tgblthelfgott  47939  vopnbgrelself  47979  clnbgr3stgrgrlic  48144  clcllaw  48315  ztprmneprm  48471  lcoel0  48553  linindslinci  48573  fv2arycl  48773