Theorem 3impib 1132

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 1126	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1103

This theorem is referenced by:  3impia  1133  mob  3683  eqreu  3695  dedth3h  4544  prproe  4866  rbropap  5539  breldmg  5890  ssimaexg  6957  funopdmsn  7137  fpr3g  8270  wfr3g  8304  dfsmo2  8322  omwordri  8545  3ecoptocl  8795  ttrclselem2  9683  frr3g  9716  cfslb  10238  cofsmo  10241  cfsmolem  10242  coftr  10245  domtriomlem  10414  zorn2lem7  10474  ttukey2g  10488  gchi  10597  tskxpss  10745  tskord  10753  infm3  12165  uzind  12679  fzind  12685  fnn0ind  12686  xltnegi  13233  axdc4uz  14011  facwordi  14316  swrdnd2  14683  cshwidxmod  14830  relexpsucl  15058  relexpsucr  15059  relexprelg  15065  relexpaddnn  15078  caubnd  15400  mulgcd  16596  lcmfdvds  16690  lcmfdvdsb  16691  coprmdvds1  16700  pcfac  16949  ramz  17075  imasleval  17585  cictr  17852  initoeu2lem1  18061  drsdir  18348  psasym  18622  pstr  18623  tsrlin  18631  dirge  18649  mgmcl  18691  mgmhmlin  18747  issubmgm2  18751  mhmlin  18841  mhmmulg  19172  issubg2  19199  nsgbi  19214  gsumcom2  20036  srgmulgass  20290  dvdsrtr  20441  rnghmmul  20522  issubrng2  20634  issubrg2  20668  domnmuln0  20785  drnginvrcl  20827  drnginvrn0  20828  drnginvrl  20830  drnginvrr  20831  isdrngd  20838  isdrngdOLD  20840  abvmul  20893  abvtri  20894  lmhmlin  21125  ipcj  21744  cssincl  21798  obsip  21831  decpmatmulsumfsupp  22891  mp2pm2mplem4  22927  pm2mpghm  22934  pm2mpmhmlem1  22936  inopn  23017  basis1  23068  iscldtop  23213  2ndcdisj  23574  cnmpt2t  23791  cnmpt22  23792  cnmptcom  23796  fbasssin  23954  ptcmplem3  24172  xmeteq0  24456  prdsxmslem2  24647  nmvs  24794  nmolb  24835  volfiniun  25667  sincosq1sgn  26621  sincosq2sgn  26622  sincosq3sgn  26623  sincosq4sgn  26624  addsproplem2  28121  negsproplem2  28180  negsid  28192  mulsproplem9  28275  precsexlem10  28367  uzsind  28556  recut  28645  ewlkle  29864  wwlksnext  30151  umgr2adedgwlklem  30202  elwwlks2ons3im  30212  usgrwwlks2on  30216  umgrwwlks2on  30217  conngrv2edg  30455  frgrwopregasn  30576  frgrwopregbsn  30577  frgrwopreglem5  30581  frgrwopreglem5ALT  30582  frgr2wwlkeu  30587  ablocom  30809  nmcvcn  30956  ipassi  31102  htth  31179  shaddcl  31478  shmulcl  31479  shsubcl  31481  chlimi  31495  pjspansn  31838  cnopc  32174  cnfnc  32191  adj1  32194  lnfnmul  32309  atord  32649  atcvat2  32650  cdj3i  32702  nexple  33090  signstfvc  34878  bnj910  35253  bnj1154  35304  r1filimi  35411  umgr2cycllem  35503  pconncn  35587  mrsubccat  35881  shftvalg  36095  linethru  36516  sin2h  38121  cos2h  38122  tan2h  38123  dvasin  38215  areacirclem1  38219  riotasv  39595  lsmsatcv  39646  omllaw  39879  2llnjN  40203  dalawlem10  40516  dalawlem13  40519  dalawlem14  40520  pclfinclN  40586  ismrc  43294  fzsplit1nn0  43347  pell1234qrmulcl  43444  pell14qrmulcl  43452  onsucf1olem  43859  iunrelexp0  44290  bi23impib  45060  bi13impib  45061  trelded  45139  suctrALT  45399  suctrALTcf  45495  suctrALTcfVD  45496  stoweidlem17  46589  zm1nn  47894  bgoldbtbndlem4  48428  bgoldbtbnd  48429  tgblthelfgott  48435  vopnbgrelself  48475  clnbgr3stgrgrlic  48640  clcllaw  48811  ztprmneprm  48978  lcoel0  49059  linindslinci  49079  fv2arycl  49279