Theorem 3impib 1128

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3impia  1129  mob  3679  eqreu  3691  dedth3h  4540  prproe  4862  rbropap  5532  breldmg  5883  ssimaexg  6949  funopdmsn  7129  fpr3g  8261  wfr3g  8295  dfsmo2  8313  omwordri  8536  3ecoptocl  8786  ttrclselem2  9678  frr3g  9711  cfslb  10220  cofsmo  10223  cfsmolem  10224  coftr  10227  domtriomlem  10396  zorn2lem7  10456  ttukey2g  10470  gchi  10579  tskxpss  10727  tskord  10735  infm3  12148  uzind  12662  fzind  12668  fnn0ind  12669  xltnegi  13216  axdc4uz  13994  facwordi  14299  swrdnd2  14666  cshwidxmod  14813  relexpsucl  15041  relexpsucr  15042  relexprelg  15048  relexpaddnn  15061  caubnd  15369  mulgcd  16565  lcmfdvds  16659  lcmfdvdsb  16660  coprmdvds1  16669  pcfac  16918  ramz  17044  imasleval  17554  cictr  17821  initoeu2lem1  18030  drsdir  18317  psasym  18591  pstr  18592  tsrlin  18600  dirge  18618  mgmcl  18660  mgmhmlin  18716  issubmgm2  18720  mhmlin  18810  mhmmulg  19140  issubg2  19166  nsgbi  19181  gsumcom2  19998  srgmulgass  20246  dvdsrtr  20396  rnghmmul  20477  issubrng2  20587  issubrg2  20621  domnmuln0  20738  drnginvrcl  20782  drnginvrn0  20783  drnginvrl  20785  drnginvrr  20786  isdrngd  20794  isdrngdOLD  20796  abvmul  20850  abvtri  20851  lmhmlin  21082  ipcj  21666  cssincl  21720  obsip  21753  decpmatmulsumfsupp  22813  mp2pm2mplem4  22849  pm2mpghm  22856  pm2mpmhmlem1  22858  inopn  22939  basis1  22990  iscldtop  23135  2ndcdisj  23496  cnmpt2t  23713  cnmpt22  23714  cnmptcom  23718  fbasssin  23876  ptcmplem3  24094  xmeteq0  24378  prdsxmslem2  24569  nmvs  24716  nmolb  24757  volfiniun  25589  sincosq1sgn  26540  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  addsproplem2  28040  negsproplem2  28099  negsid  28111  mulsproplem9  28194  precsexlem10  28286  uzsind  28475  recut  28564  ewlkle  29752  wwlksnext  30039  umgr2adedgwlklem  30090  elwwlks2ons3im  30100  usgrwwlks2on  30104  umgrwwlks2on  30105  conngrv2edg  30343  frgrwopregasn  30464  frgrwopregbsn  30465  frgrwopreglem5  30469  frgrwopreglem5ALT  30470  frgr2wwlkeu  30475  ablocom  30697  nmcvcn  30844  ipassi  30990  htth  31067  shaddcl  31366  shmulcl  31367  shsubcl  31369  chlimi  31383  pjspansn  31726  cnopc  32062  cnfnc  32079  adj1  32082  lnfnmul  32197  atord  32537  atcvat2  32538  cdj3i  32590  nexple  32996  signstfvc  34832  bnj910  35207  bnj1154  35258  r1filimi  35363  umgr2cycllem  35454  pconncn  35538  mrsubccat  35832  shftvalg  36046  linethru  36467  sin2h  38073  cos2h  38074  tan2h  38075  dvasin  38167  areacirclem1  38171  riotasv  39547  lsmsatcv  39598  omllaw  39831  2llnjN  40155  dalawlem10  40468  dalawlem13  40471  dalawlem14  40472  pclfinclN  40538  ismrc  43246  fzsplit1nn0  43299  pell1234qrmulcl  43396  pell14qrmulcl  43404  onsucf1olem  43811  iunrelexp0  44242  bi23impib  45026  bi13impib  45027  trelded  45105  suctrALT  45365  suctrALTcf  45461  suctrALTcfVD  45462  stoweidlem17  46555  zm1nn  47860  bgoldbtbndlem4  48394  bgoldbtbnd  48395  tgblthelfgott  48401  vopnbgrelself  48441  clnbgr3stgrgrlic  48606  clcllaw  48777  ztprmneprm  48933  lcoel0  49014  linindslinci  49034  fv2arycl  49234