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  4865  rbropap  5538  breldmg  5889  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  12162  uzind  12676  fzind  12682  fnn0ind  12683  xltnegi  13230  axdc4uz  14008  facwordi  14313  swrdnd2  14681  cshwidxmod  14828  relexpsucl  15056  relexpsucr  15057  relexprelg  15063  relexpaddnn  15076  caubnd  15398  mulgcd  16594  lcmfdvds  16688  lcmfdvdsb  16689  coprmdvds1  16698  pcfac  16947  ramz  17073  imasleval  17583  cictr  17850  initoeu2lem1  18059  drsdir  18346  psasym  18620  pstr  18621  tsrlin  18629  dirge  18647  mgmcl  18689  mgmhmlin  18745  issubmgm2  18749  mhmlin  18839  mhmmulg  19169  issubg2  19196  nsgbi  19211  gsumcom2  20033  srgmulgass  20287  dvdsrtr  20438  rnghmmul  20519  issubrng2  20631  issubrg2  20665  domnmuln0  20782  drnginvrcl  20824  drnginvrn0  20825  drnginvrl  20827  drnginvrr  20828  isdrngd  20835  isdrngdOLD  20837  abvmul  20890  abvtri  20891  lmhmlin  21122  ipcj  21741  cssincl  21795  obsip  21828  decpmatmulsumfsupp  22887  mp2pm2mplem4  22923  pm2mpghm  22930  pm2mpmhmlem1  22932  inopn  23013  basis1  23064  iscldtop  23209  2ndcdisj  23570  cnmpt2t  23787  cnmpt22  23788  cnmptcom  23792  fbasssin  23950  ptcmplem3  24168  xmeteq0  24452  prdsxmslem2  24643  nmvs  24790  nmolb  24831  volfiniun  25663  sincosq1sgn  26617  sincosq2sgn  26618  sincosq3sgn  26619  sincosq4sgn  26620  addsproplem2  28117  negsproplem2  28176  negsid  28188  mulsproplem9  28271  precsexlem10  28363  uzsind  28552  recut  28641  ewlkle  29860  wwlksnext  30147  umgr2adedgwlklem  30198  elwwlks2ons3im  30208  usgrwwlks2on  30212  umgrwwlks2on  30213  conngrv2edg  30451  frgrwopregasn  30572  frgrwopregbsn  30573  frgrwopreglem5  30577  frgrwopreglem5ALT  30578  frgr2wwlkeu  30583  ablocom  30805  nmcvcn  30952  ipassi  31098  htth  31175  shaddcl  31474  shmulcl  31475  shsubcl  31477  chlimi  31491  pjspansn  31834  cnopc  32170  cnfnc  32187  adj1  32190  lnfnmul  32305  atord  32645  atcvat2  32646  cdj3i  32698  nexple  33085  signstfvc  34873  bnj910  35248  bnj1154  35299  r1filimi  35406  umgr2cycllem  35498  pconncn  35582  mrsubccat  35876  shftvalg  36090  linethru  36511  sin2h  38116  cos2h  38117  tan2h  38118  dvasin  38210  areacirclem1  38214  riotasv  39590  lsmsatcv  39641  omllaw  39874  2llnjN  40198  dalawlem10  40511  dalawlem13  40514  dalawlem14  40515  pclfinclN  40581  ismrc  43289  fzsplit1nn0  43342  pell1234qrmulcl  43439  pell14qrmulcl  43447  onsucf1olem  43854  iunrelexp0  44285  bi23impib  45054  bi13impib  45055  trelded  45133  suctrALT  45393  suctrALTcf  45489  suctrALTcfVD  45490  stoweidlem17  46590  zm1nn  47895  bgoldbtbndlem4  48429  bgoldbtbnd  48430  tgblthelfgott  48436  vopnbgrelself  48476  clnbgr3stgrgrlic  48641  clcllaw  48812  ztprmneprm  48979  lcoel0  49060  linindslinci  49080  fv2arycl  49280