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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  3impia  1118  mob  3714  eqreu  3726  dedth3h  4589  prproe  4907  rbropap  5566  breldmg  5910  ssimaexg  6978  funopdmsn  7148  fpr3g  8270  wfr3g  8307  dfsmo2  8347  omwordri  8572  3ecoptocl  8803  ttrclselem2  9721  frr3g  9751  cfslb  10261  cofsmo  10264  cfsmolem  10265  coftr  10268  domtriomlem  10437  zorn2lem7  10497  ttukey2g  10511  gchi  10619  tskxpss  10767  tskord  10775  infm3  12173  uzind  12654  fzind  12660  fnn0ind  12661  xltnegi  13195  axdc4uz  13949  facwordi  14249  swrdnd2  14605  cshwidxmod  14753  relexpsucl  14978  relexpsucr  14979  relexprelg  14985  relexpaddnn  14998  caubnd  15305  mulgcd  16490  lcmfdvds  16579  lcmfdvdsb  16580  coprmdvds1  16589  pcfac  16832  ramz  16958  imasleval  17487  cictr  17752  initoeu2lem1  17964  drsdir  18255  psasym  18529  pstr  18530  tsrlin  18538  dirge  18556  mgmcl  18564  mhmlin  18679  mhmmulg  18995  issubg2  19021  nsgbi  19037  gsumcom2  19843  srgmulgass  20040  dvdsrtr  20182  issubrg2  20339  drnginvrcl  20379  drnginvrn0  20380  drnginvrl  20382  drnginvrr  20383  isdrngd  20390  isdrngdOLD  20392  abvmul  20437  abvtri  20438  lmhmlin  20646  domnmuln0  20914  ipcj  21187  cssincl  21241  obsip  21276  decpmatmulsumfsupp  22275  mp2pm2mplem4  22311  pm2mpghm  22318  pm2mpmhmlem1  22320  inopn  22401  basis1  22453  iscldtop  22599  2ndcdisj  22960  cnmpt2t  23177  cnmpt22  23178  cnmptcom  23182  fbasssin  23340  ptcmplem3  23558  xmeteq0  23844  prdsxmslem2  24038  nmvs  24193  nmolb  24234  volfiniun  25064  sincosq1sgn  26008  sincosq2sgn  26009  sincosq3sgn  26010  sincosq4sgn  26011  ssltsn  27294  addsproplem2  27456  negsproplem2  27506  negsid  27518  mulsproplem9  27583  precsexlem10  27665  ewlkle  28893  wwlksnext  29178  umgr2adedgwlklem  29229  elwwlks2ons3im  29239  umgrwwlks2on  29242  conngrv2edg  29479  frgrwopregasn  29600  frgrwopregbsn  29601  frgrwopreglem5  29605  frgrwopreglem5ALT  29606  frgr2wwlkeu  29611  ablocom  29832  nmcvcn  29979  ipassi  30125  htth  30202  shaddcl  30501  shmulcl  30502  shsubcl  30504  chlimi  30518  pjspansn  30861  cnopc  31197  cnfnc  31214  adj1  31217  lnfnmul  31332  atord  31672  atcvat2  31673  cdj3i  31725  nexple  33038  signstfvc  33616  bnj910  33990  bnj1154  34041  umgr2cycllem  34162  pconncn  34246  mrsubccat  34540  shftvalg  34732  linethru  35156  sin2h  36526  cos2h  36527  tan2h  36528  dvasin  36620  areacirclem1  36624  riotasv  37877  lsmsatcv  37928  omllaw  38161  2llnjN  38486  dalawlem10  38799  dalawlem13  38802  dalawlem14  38803  pclfinclN  38869  ismrc  41487  fzsplit1nn0  41540  pell1234qrmulcl  41641  pell14qrmulcl  41649  onsucf1olem  42068  iunrelexp0  42501  bi23impib  43294  bi13impib  43295  trelded  43374  suctrALT  43635  suctrALTcf  43731  suctrALTcfVD  43732  stoweidlem17  44781  zm1nn  46058  bgoldbtbndlem4  46524  bgoldbtbnd  46525  tgblthelfgott  46531  mgmhmlin  46604  issubmgm2  46608  clcllaw  46649  rnghmmul  46746  issubrng2  46785  ztprmneprm  47071  lcoel0  47157  linindslinci  47177  fv2arycl  47382