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  3675  eqreu  3687  dedth3h  4540  prproe  4861  rbropap  5511  breldmg  5858  ssimaexg  6920  funopdmsn  7095  fpr3g  8227  wfr3g  8261  dfsmo2  8279  omwordri  8499  3ecoptocl  8746  ttrclselem2  9635  frr3g  9668  cfslb  10176  cofsmo  10179  cfsmolem  10180  coftr  10183  domtriomlem  10352  zorn2lem7  10412  ttukey2g  10426  gchi  10535  tskxpss  10683  tskord  10691  infm3  12101  uzind  12584  fzind  12590  fnn0ind  12591  xltnegi  13131  axdc4uz  13907  facwordi  14212  swrdnd2  14579  cshwidxmod  14726  relexpsucl  14954  relexpsucr  14955  relexprelg  14961  relexpaddnn  14974  caubnd  15282  mulgcd  16475  lcmfdvds  16569  lcmfdvdsb  16570  coprmdvds1  16579  pcfac  16827  ramz  16953  imasleval  17462  cictr  17729  initoeu2lem1  17938  drsdir  18225  psasym  18499  pstr  18500  tsrlin  18508  dirge  18526  mgmcl  18568  mgmhmlin  18624  issubmgm2  18628  mhmlin  18718  mhmmulg  19045  issubg2  19071  nsgbi  19086  gsumcom2  19904  srgmulgass  20152  dvdsrtr  20304  rnghmmul  20385  issubrng2  20491  issubrg2  20525  domnmuln0  20642  drnginvrcl  20686  drnginvrn0  20687  drnginvrl  20689  drnginvrr  20690  isdrngd  20698  isdrngdOLD  20700  abvmul  20754  abvtri  20755  lmhmlin  20987  ipcj  21589  cssincl  21643  obsip  21676  decpmatmulsumfsupp  22717  mp2pm2mplem4  22753  pm2mpghm  22760  pm2mpmhmlem1  22762  inopn  22843  basis1  22894  iscldtop  23039  2ndcdisj  23400  cnmpt2t  23617  cnmpt22  23618  cnmptcom  23622  fbasssin  23780  ptcmplem3  23998  xmeteq0  24282  prdsxmslem2  24473  nmvs  24620  nmolb  24661  volfiniun  25504  sincosq1sgn  26463  sincosq2sgn  26464  sincosq3sgn  26465  sincosq4sgn  26466  addsproplem2  27966  negsproplem2  28025  negsid  28037  mulsproplem9  28120  precsexlem10  28212  uzsind  28401  recut  28490  ewlkle  29679  wwlksnext  29966  umgr2adedgwlklem  30017  elwwlks2ons3im  30027  usgrwwlks2on  30031  umgrwwlks2on  30032  conngrv2edg  30270  frgrwopregasn  30391  frgrwopregbsn  30392  frgrwopreglem5  30396  frgrwopreglem5ALT  30397  frgr2wwlkeu  30402  ablocom  30623  nmcvcn  30770  ipassi  30916  htth  30993  shaddcl  31292  shmulcl  31293  shsubcl  31295  chlimi  31309  pjspansn  31652  cnopc  31988  cnfnc  32005  adj1  32008  lnfnmul  32123  atord  32463  atcvat2  32464  cdj3i  32516  nexple  32925  signstfvc  34731  bnj910  35104  bnj1154  35155  r1filimi  35259  umgr2cycllem  35334  pconncn  35418  mrsubccat  35712  shftvalg  35926  linethru  36347  sin2h  37807  cos2h  37808  tan2h  37809  dvasin  37901  areacirclem1  37905  riotasv  39215  lsmsatcv  39266  omllaw  39499  2llnjN  39823  dalawlem10  40136  dalawlem13  40139  dalawlem14  40140  pclfinclN  40206  ismrc  42939  fzsplit1nn0  42992  pell1234qrmulcl  43093  pell14qrmulcl  43101  onsucf1olem  43508  iunrelexp0  43939  bi23impib  44723  bi13impib  44724  trelded  44802  suctrALT  45062  suctrALTcf  45158  suctrALTcfVD  45159  stoweidlem17  46257  zm1nn  47544  bgoldbtbndlem4  48050  bgoldbtbnd  48051  tgblthelfgott  48057  vopnbgrelself  48097  clnbgr3stgrgrlic  48262  clcllaw  48433  ztprmneprm  48589  lcoel0  48670  linindslinci  48690  fv2arycl  48890