Theorem 3impib 1122

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3impia  1123  mob  3665  eqreu  3677  dedth3h  4522  prproe  4843  rbropap  5512  breldmg  5858  ssimaexg  6920  funopdmsn  7100  fpr3g  8232  wfr3g  8266  dfsmo2  8284  omwordri  8504  3ecoptocl  8753  ttrclselem2  9645  frr3g  9678  cfslb  10186  cofsmo  10189  cfsmolem  10190  coftr  10193  domtriomlem  10362  zorn2lem7  10422  ttukey2g  10436  gchi  10545  tskxpss  10693  tskord  10701  infm3  12113  uzind  12619  fzind  12625  fnn0ind  12626  xltnegi  13166  axdc4uz  13944  facwordi  14249  swrdnd2  14616  cshwidxmod  14763  relexpsucl  14991  relexpsucr  14992  relexprelg  14998  relexpaddnn  15011  caubnd  15319  mulgcd  16515  lcmfdvds  16609  lcmfdvdsb  16610  coprmdvds1  16619  pcfac  16868  ramz  16994  imasleval  17503  cictr  17770  initoeu2lem1  17979  drsdir  18266  psasym  18540  pstr  18541  tsrlin  18549  dirge  18567  mgmcl  18609  mgmhmlin  18665  issubmgm2  18669  mhmlin  18759  mhmmulg  19089  issubg2  19115  nsgbi  19130  gsumcom2  19948  srgmulgass  20196  dvdsrtr  20346  rnghmmul  20427  issubrng2  20537  issubrg2  20571  domnmuln0  20688  drnginvrcl  20732  drnginvrn0  20733  drnginvrl  20735  drnginvrr  20736  isdrngd  20744  isdrngdOLD  20746  abvmul  20800  abvtri  20801  lmhmlin  21032  ipcj  21616  cssincl  21670  obsip  21703  decpmatmulsumfsupp  22763  mp2pm2mplem4  22799  pm2mpghm  22806  pm2mpmhmlem1  22808  inopn  22889  basis1  22940  iscldtop  23085  2ndcdisj  23446  cnmpt2t  23663  cnmpt22  23664  cnmptcom  23668  fbasssin  23826  ptcmplem3  24044  xmeteq0  24328  prdsxmslem2  24519  nmvs  24666  nmolb  24707  volfiniun  25539  sincosq1sgn  26487  sincosq2sgn  26488  sincosq3sgn  26489  sincosq4sgn  26490  addsproplem2  27987  negsproplem2  28046  negsid  28058  mulsproplem9  28141  precsexlem10  28233  uzsind  28422  recut  28511  ewlkle  29699  wwlksnext  29986  umgr2adedgwlklem  30037  elwwlks2ons3im  30047  usgrwwlks2on  30051  umgrwwlks2on  30052  conngrv2edg  30290  frgrwopregasn  30411  frgrwopregbsn  30412  frgrwopreglem5  30416  frgrwopreglem5ALT  30417  frgr2wwlkeu  30422  ablocom  30644  nmcvcn  30791  ipassi  30937  htth  31014  shaddcl  31313  shmulcl  31314  shsubcl  31316  chlimi  31330  pjspansn  31673  cnopc  32009  cnfnc  32026  adj1  32029  lnfnmul  32144  atord  32484  atcvat2  32485  cdj3i  32537  nexple  32943  signstfvc  34765  bnj910  35137  bnj1154  35188  r1filimi  35291  umgr2cycllem  35375  pconncn  35459  mrsubccat  35753  shftvalg  35967  linethru  36388  sin2h  37984  cos2h  37985  tan2h  37986  dvasin  38078  areacirclem1  38082  riotasv  39458  lsmsatcv  39509  omllaw  39742  2llnjN  40066  dalawlem10  40379  dalawlem13  40382  dalawlem14  40383  pclfinclN  40449  ismrc  43157  fzsplit1nn0  43210  pell1234qrmulcl  43307  pell14qrmulcl  43315  onsucf1olem  43722  iunrelexp0  44153  bi23impib  44937  bi13impib  44938  trelded  45016  suctrALT  45276  suctrALTcf  45372  suctrALTcfVD  45373  stoweidlem17  46467  zm1nn  47772  bgoldbtbndlem4  48306  bgoldbtbnd  48307  tgblthelfgott  48313  vopnbgrelself  48353  clnbgr3stgrgrlic  48518  clcllaw  48689  ztprmneprm  48845  lcoel0  48926  linindslinci  48946  fv2arycl  49146