Theorem 3impib 1134

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  3impia  1135  mob  3681  eqreu  3693  dedth3h  4549  prproe  4871  rbropap  5550  breldmg  5901  ssimaexg  6969  funopdmsn  7149  fpr3g  8283  wfr3g  8317  dfsmo2  8335  omwordri  8558  3ecoptocl  8808  ttrclselem2  9696  frr3g  9729  cfslb  10251  cofsmo  10254  cfsmolem  10255  coftr  10258  domtriomlem  10427  zorn2lem7  10487  ttukey2g  10501  gchi  10610  tskxpss  10758  tskord  10766  infm3  12175  uzind  12689  fzind  12695  fnn0ind  12696  xltnegi  13243  axdc4uz  14022  facwordi  14327  swrdnd2  14695  cshwidxmod  14842  relexpsucl  15070  relexpsucr  15071  relexprelg  15077  relexpaddnn  15090  caubnd  15412  mulgcd  16607  lcmfdvds  16701  lcmfdvdsb  16702  coprmdvds1  16711  pcfac  16960  ramz  17086  imasleval  17596  cictr  17863  initoeu2lem1  18072  drsdir  18359  psasym  18633  pstr  18634  tsrlin  18642  dirge  18660  mgmcl  18702  mgmhmlin  18758  issubmgm2  18762  mhmlin  18852  mhmmulg  19182  issubg2  19209  nsgbi  19224  gsumcom2  20046  srgmulgass  20300  dvdsrtr  20451  rnghmmul  20532  issubrng2  20644  issubrg2  20678  domnmuln0  20795  drnginvrcl  20839  drnginvrn0  20840  drnginvrl  20842  drnginvrr  20843  isdrngd  20850  isdrngdOLD  20852  abvmul  20905  abvtri  20906  lmhmlin  21137  ipcj  21765  cssincl  21819  obsip  21852  decpmatmulsumfsupp  22911  mp2pm2mplem4  22947  pm2mpghm  22954  pm2mpmhmlem1  22956  inopn  23037  basis1  23088  iscldtop  23233  2ndcdisj  23594  cnmpt2t  23811  cnmpt22  23812  cnmptcom  23816  fbasssin  23974  ptcmplem3  24192  xmeteq0  24476  prdsxmslem2  24667  nmvs  24814  nmolb  24855  volfiniun  25687  sincosq1sgn  26641  sincosq2sgn  26642  sincosq3sgn  26643  sincosq4sgn  26644  addsproplem2  28141  negsproplem2  28200  negsid  28212  mulsproplem9  28295  precsexlem10  28387  uzsind  28576  recut  28665  ewlkle  29933  wwlksnext  30220  umgr2adedgwlklem  30271  elwwlks2ons3im  30281  usgrwwlks2on  30285  umgrwwlks2on  30286  conngrv2edg  30524  frgrwopregasn  30645  frgrwopregbsn  30646  frgrwopreglem5  30650  frgrwopreglem5ALT  30651  frgr2wwlkeu  30656  ablocom  30878  nmcvcn  31025  ipassi  31171  htth  31248  shaddcl  31547  shmulcl  31548  shsubcl  31550  chlimi  31564  pjspansn  31907  cnopc  32243  cnfnc  32260  adj1  32263  lnfnmul  32378  atord  32718  atcvat2  32719  cdj3i  32771  nexple  33155  signstfvc  34939  bnj910  35314  bnj1154  35365  r1filimi  35475  umgr2cycllem  35610  pconncn  35694  mrsubccat  35988  shftvalg  36202  linethru  36623  sin2h  38239  cos2h  38240  tan2h  38241  dvasin  38333  areacirclem1  38337  riotasv  39711  lsmsatcv  39762  omllaw  39995  2llnjN  40319  dalawlem10  40632  dalawlem13  40635  dalawlem14  40636  pclfinclN  40702  ismrc  43412  fzsplit1nn0  43465  pell1234qrmulcl  43562  pell14qrmulcl  43570  onsucf1olem  43977  iunrelexp0  44408  bi23impib  45175  bi13impib  45176  trelded  45254  suctrALT  45514  suctrALTcf  45610  suctrALTcfVD  45611  stoweidlem17  46711  zm1nn  48016  bgoldbtbndlem4  48550  bgoldbtbnd  48551  tgblthelfgott  48557  vopnbgrelself  48597  clnbgr3stgrgrlic  48762  clcllaw  48933  ztprmneprm  49104  lcoel0  49185  linindslinci  49205  fv2arycl  49405