Theorem 3impib 1117

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3impia  1118  mob  3677  eqreu  3689  dedth3h  4542  prproe  4863  rbropap  5519  breldmg  5866  ssimaexg  6928  funopdmsn  7105  fpr3g  8237  wfr3g  8271  dfsmo2  8289  omwordri  8509  3ecoptocl  8758  ttrclselem2  9647  frr3g  9680  cfslb  10188  cofsmo  10191  cfsmolem  10192  coftr  10195  domtriomlem  10364  zorn2lem7  10424  ttukey2g  10438  gchi  10547  tskxpss  10695  tskord  10703  infm3  12113  uzind  12596  fzind  12602  fnn0ind  12603  xltnegi  13143  axdc4uz  13919  facwordi  14224  swrdnd2  14591  cshwidxmod  14738  relexpsucl  14966  relexpsucr  14967  relexprelg  14973  relexpaddnn  14986  caubnd  15294  mulgcd  16487  lcmfdvds  16581  lcmfdvdsb  16582  coprmdvds1  16591  pcfac  16839  ramz  16965  imasleval  17474  cictr  17741  initoeu2lem1  17950  drsdir  18237  psasym  18511  pstr  18512  tsrlin  18520  dirge  18538  mgmcl  18580  mgmhmlin  18636  issubmgm2  18640  mhmlin  18730  mhmmulg  19057  issubg2  19083  nsgbi  19098  gsumcom2  19916  srgmulgass  20164  dvdsrtr  20316  rnghmmul  20397  issubrng2  20503  issubrg2  20537  domnmuln0  20654  drnginvrcl  20698  drnginvrn0  20699  drnginvrl  20701  drnginvrr  20702  isdrngd  20710  isdrngdOLD  20712  abvmul  20766  abvtri  20767  lmhmlin  20999  ipcj  21601  cssincl  21655  obsip  21688  decpmatmulsumfsupp  22729  mp2pm2mplem4  22765  pm2mpghm  22772  pm2mpmhmlem1  22774  inopn  22855  basis1  22906  iscldtop  23051  2ndcdisj  23412  cnmpt2t  23629  cnmpt22  23630  cnmptcom  23634  fbasssin  23792  ptcmplem3  24010  xmeteq0  24294  prdsxmslem2  24485  nmvs  24632  nmolb  24673  volfiniun  25516  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  addsproplem2  27978  negsproplem2  28037  negsid  28049  mulsproplem9  28132  precsexlem10  28224  uzsind  28413  recut  28502  ewlkle  29691  wwlksnext  29978  umgr2adedgwlklem  30029  elwwlks2ons3im  30039  usgrwwlks2on  30043  umgrwwlks2on  30044  conngrv2edg  30282  frgrwopregasn  30403  frgrwopregbsn  30404  frgrwopreglem5  30408  frgrwopreglem5ALT  30409  frgr2wwlkeu  30414  ablocom  30635  nmcvcn  30782  ipassi  30928  htth  31005  shaddcl  31304  shmulcl  31305  shsubcl  31307  chlimi  31321  pjspansn  31664  cnopc  32000  cnfnc  32017  adj1  32020  lnfnmul  32135  atord  32475  atcvat2  32476  cdj3i  32528  nexple  32935  signstfvc  34751  bnj910  35123  bnj1154  35174  r1filimi  35278  umgr2cycllem  35353  pconncn  35437  mrsubccat  35731  shftvalg  35945  linethru  36366  sin2h  37855  cos2h  37856  tan2h  37857  dvasin  37949  areacirclem1  37953  riotasv  39329  lsmsatcv  39380  omllaw  39613  2llnjN  39937  dalawlem10  40250  dalawlem13  40253  dalawlem14  40254  pclfinclN  40320  ismrc  43052  fzsplit1nn0  43105  pell1234qrmulcl  43206  pell14qrmulcl  43214  onsucf1olem  43621  iunrelexp0  44052  bi23impib  44836  bi13impib  44837  trelded  44915  suctrALT  45175  suctrALTcf  45271  suctrALTcfVD  45272  stoweidlem17  46369  zm1nn  47656  bgoldbtbndlem4  48162  bgoldbtbnd  48163  tgblthelfgott  48169  vopnbgrelself  48209  clnbgr3stgrgrlic  48374  clcllaw  48545  ztprmneprm  48701  lcoel0  48782  linindslinci  48802  fv2arycl  49002