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  3662  eqreu  3674  dedth3h  4531  prproe  4848  rbropap  5498  breldmg  5838  ssimaexg  6893  funopdmsn  7061  fpr3g  8148  wfr3g  8185  dfsmo2  8225  omwordri  8451  3ecoptocl  8646  ttrclselem2  9555  frr3g  9585  cfslb  10095  cofsmo  10098  cfsmolem  10099  coftr  10102  domtriomlem  10271  zorn2lem7  10331  ttukey2g  10345  gchi  10453  tskxpss  10601  tskord  10609  infm3  12007  uzind  12485  fzind  12491  fnn0ind  12492  xltnegi  13023  axdc4uz  13777  facwordi  14076  swrdnd2  14440  cshwidxmod  14588  relexpsucl  14814  relexpsucr  14815  relexprelg  14821  relexpaddnn  14834  caubnd  15142  mulgcd  16328  lcmfdvds  16417  lcmfdvdsb  16418  coprmdvds1  16427  pcfac  16670  ramz  16796  imasleval  17322  cictr  17587  initoeu2lem1  17799  drsdir  18090  psasym  18364  pstr  18365  tsrlin  18373  dirge  18391  mgmcl  18399  mhmlin  18507  mhmmulg  18813  issubg2  18839  nsgbi  18854  cygablOLD  19560  gsumcom2  19644  srgmulgass  19835  dvdsrtr  19962  drnginvrcl  20080  drnginvrn0  20081  drnginvrl  20082  drnginvrr  20083  isdrngd  20088  issubrg2  20116  abvmul  20161  abvtri  20162  lmhmlin  20369  domnmuln0  20641  ipcj  20911  cssincl  20965  obsip  21000  decpmatmulsumfsupp  21994  mp2pm2mplem4  22030  pm2mpghm  22037  pm2mpmhmlem1  22039  inopn  22120  basis1  22172  iscldtop  22318  2ndcdisj  22679  cnmpt2t  22896  cnmpt22  22897  cnmptcom  22901  fbasssin  23059  ptcmplem3  23277  xmeteq0  23563  prdsxmslem2  23757  nmvs  23912  nmolb  23953  volfiniun  24783  sincosq1sgn  25727  sincosq2sgn  25728  sincosq3sgn  25729  sincosq4sgn  25730  ewlkle  28081  wwlksnext  28367  umgr2adedgwlklem  28418  elwwlks2ons3im  28428  umgrwwlks2on  28431  conngrv2edg  28668  frgrwopregasn  28789  frgrwopregbsn  28790  frgrwopreglem5  28794  frgrwopreglem5ALT  28795  frgr2wwlkeu  28800  ablocom  29019  nmcvcn  29166  ipassi  29312  htth  29389  shaddcl  29688  shmulcl  29689  shsubcl  29691  chlimi  29705  pjspansn  30048  cnopc  30384  cnfnc  30401  adj1  30404  lnfnmul  30519  atord  30859  atcvat2  30860  cdj3i  30912  nexple  32083  signstfvc  32659  bnj910  33033  bnj1154  33084  umgr2cycllem  33207  pconncn  33291  mrsubccat  33585  shftvalg  33798  linethru  34513  sin2h  35823  cos2h  35824  tan2h  35825  dvasin  35917  areacirclem1  35921  riotasv  37177  lsmsatcv  37228  omllaw  37461  2llnjN  37786  dalawlem10  38099  dalawlem13  38102  dalawlem14  38103  pclfinclN  38169  ismrc  40726  fzsplit1nn0  40779  pell1234qrmulcl  40880  pell14qrmulcl  40888  iunrelexp0  41531  bi23impib  42326  bi13impib  42327  trelded  42406  suctrALT  42667  suctrALTcf  42763  suctrALTcfVD  42764  stoweidlem17  43795  zm1nn  45046  bgoldbtbndlem4  45512  bgoldbtbnd  45513  tgblthelfgott  45519  mgmhmlin  45592  issubmgm2  45596  clcllaw  45637  rnghmmul  45710  ztprmneprm  45935  lcoel0  46021  linindslinci  46041  fv2arycl  46246