Theorem 3impib 1115

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3impia  1116  mob  3652  eqreu  3664  dedth3h  4519  prproe  4837  rbropap  5478  breldmg  5818  ssimaexg  6854  funopdmsn  7022  fpr3g  8101  wfr3g  8138  dfsmo2  8178  omwordri  8403  3ecoptocl  8598  ttrclselem2  9484  frr3g  9514  cfslb  10022  cofsmo  10025  cfsmolem  10026  coftr  10029  domtriomlem  10198  zorn2lem7  10258  ttukey2g  10272  gchi  10380  tskxpss  10528  tskord  10536  infm3  11934  uzind  12412  fzind  12418  fnn0ind  12419  xltnegi  12950  axdc4uz  13704  facwordi  14003  swrdnd2  14368  cshwidxmod  14516  relexpsucl  14742  relexpsucr  14743  relexprelg  14749  relexpaddnn  14762  caubnd  15070  mulgcd  16256  lcmfdvds  16347  lcmfdvdsb  16348  coprmdvds1  16357  pcfac  16600  ramz  16726  imasleval  17252  cictr  17517  initoeu2lem1  17729  drsdir  18020  psasym  18294  pstr  18295  tsrlin  18303  dirge  18321  mgmcl  18329  mhmlin  18437  mhmmulg  18744  issubg2  18770  nsgbi  18785  cygablOLD  19492  gsumcom2  19576  srgmulgass  19767  dvdsrtr  19894  drnginvrcl  20008  drnginvrn0  20009  drnginvrl  20010  drnginvrr  20011  isdrngd  20016  issubrg2  20044  abvmul  20089  abvtri  20090  lmhmlin  20297  domnmuln0  20569  ipcj  20839  cssincl  20893  obsip  20928  decpmatmulsumfsupp  21922  mp2pm2mplem4  21958  pm2mpghm  21965  pm2mpmhmlem1  21967  inopn  22048  basis1  22100  iscldtop  22246  2ndcdisj  22607  cnmpt2t  22824  cnmpt22  22825  cnmptcom  22829  fbasssin  22987  ptcmplem3  23205  xmeteq0  23491  prdsxmslem2  23685  nmvs  23840  nmolb  23881  volfiniun  24711  sincosq1sgn  25655  sincosq2sgn  25656  sincosq3sgn  25657  sincosq4sgn  25658  ewlkle  27972  wwlksnext  28258  umgr2adedgwlklem  28309  elwwlks2ons3im  28319  umgrwwlks2on  28322  conngrv2edg  28559  frgrwopregasn  28680  frgrwopregbsn  28681  frgrwopreglem5  28685  frgrwopreglem5ALT  28686  frgr2wwlkeu  28691  ablocom  28910  nmcvcn  29057  ipassi  29203  htth  29280  shaddcl  29579  shmulcl  29580  shsubcl  29582  chlimi  29596  pjspansn  29939  cnopc  30275  cnfnc  30292  adj1  30295  lnfnmul  30410  atord  30750  atcvat2  30751  cdj3i  30803  nexple  31977  signstfvc  32553  bnj910  32928  bnj1154  32979  umgr2cycllem  33102  pconncn  33186  mrsubccat  33480  shftvalg  33697  linethru  34455  sin2h  35767  cos2h  35768  tan2h  35769  dvasin  35861  areacirclem1  35865  riotasv  36973  lsmsatcv  37024  omllaw  37257  2llnjN  37581  dalawlem10  37894  dalawlem13  37897  dalawlem14  37898  pclfinclN  37964  ismrc  40523  fzsplit1nn0  40576  pell1234qrmulcl  40677  pell14qrmulcl  40685  iunrelexp0  41310  bi23impib  42105  bi13impib  42106  trelded  42185  suctrALT  42446  suctrALTcf  42542  suctrALTcfVD  42543  stoweidlem17  43558  zm1nn  44794  bgoldbtbndlem4  45260  bgoldbtbnd  45261  tgblthelfgott  45267  mgmhmlin  45340  issubmgm2  45344  clcllaw  45385  rnghmmul  45458  ztprmneprm  45683  lcoel0  45769  linindslinci  45789  fv2arycl  45994