Theorem 3impib 1116

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

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

This theorem is referenced by:  3impia  1117  mob  3691  eqreu  3703  dedth3h  4552  prproe  4872  rbropap  5528  breldmg  5876  ssimaexg  6950  funopdmsn  7125  fpr3g  8267  wfr3g  8301  dfsmo2  8319  omwordri  8539  3ecoptocl  8785  ttrclselem2  9686  frr3g  9716  cfslb  10226  cofsmo  10229  cfsmolem  10230  coftr  10233  domtriomlem  10402  zorn2lem7  10462  ttukey2g  10476  gchi  10584  tskxpss  10732  tskord  10740  infm3  12149  uzind  12633  fzind  12639  fnn0ind  12640  xltnegi  13183  axdc4uz  13956  facwordi  14261  swrdnd2  14627  cshwidxmod  14775  relexpsucl  15004  relexpsucr  15005  relexprelg  15011  relexpaddnn  15024  caubnd  15332  mulgcd  16525  lcmfdvds  16619  lcmfdvdsb  16620  coprmdvds1  16629  pcfac  16877  ramz  17003  imasleval  17511  cictr  17774  initoeu2lem1  17983  drsdir  18270  psasym  18542  pstr  18543  tsrlin  18551  dirge  18569  mgmcl  18577  mgmhmlin  18633  issubmgm2  18637  mhmlin  18727  mhmmulg  19054  issubg2  19080  nsgbi  19096  gsumcom2  19912  srgmulgass  20133  dvdsrtr  20284  rnghmmul  20365  issubrng2  20474  issubrg2  20508  domnmuln0  20625  drnginvrcl  20669  drnginvrn0  20670  drnginvrl  20672  drnginvrr  20673  isdrngd  20681  isdrngdOLD  20683  abvmul  20737  abvtri  20738  lmhmlin  20949  ipcj  21550  cssincl  21604  obsip  21637  decpmatmulsumfsupp  22667  mp2pm2mplem4  22703  pm2mpghm  22710  pm2mpmhmlem1  22712  inopn  22793  basis1  22844  iscldtop  22989  2ndcdisj  23350  cnmpt2t  23567  cnmpt22  23568  cnmptcom  23572  fbasssin  23730  ptcmplem3  23948  xmeteq0  24233  prdsxmslem2  24424  nmvs  24571  nmolb  24612  volfiniun  25455  sincosq1sgn  26414  sincosq2sgn  26415  sincosq3sgn  26416  sincosq4sgn  26417  ssltsn  27711  addsproplem2  27884  negsproplem2  27942  negsid  27954  mulsproplem9  28034  precsexlem10  28125  uzsind  28300  recut  28354  0reno  28355  ewlkle  29540  wwlksnext  29830  umgr2adedgwlklem  29881  elwwlks2ons3im  29891  umgrwwlks2on  29894  conngrv2edg  30131  frgrwopregasn  30252  frgrwopregbsn  30253  frgrwopreglem5  30257  frgrwopreglem5ALT  30258  frgr2wwlkeu  30263  ablocom  30484  nmcvcn  30631  ipassi  30777  htth  30854  shaddcl  31153  shmulcl  31154  shsubcl  31156  chlimi  31170  pjspansn  31513  cnopc  31849  cnfnc  31866  adj1  31869  lnfnmul  31984  atord  32324  atcvat2  32325  cdj3i  32377  nexple  32776  signstfvc  34572  bnj910  34945  bnj1154  34996  umgr2cycllem  35134  pconncn  35218  mrsubccat  35512  shftvalg  35726  linethru  36148  sin2h  37611  cos2h  37612  tan2h  37613  dvasin  37705  areacirclem1  37709  riotasv  38959  lsmsatcv  39010  omllaw  39243  2llnjN  39568  dalawlem10  39881  dalawlem13  39884  dalawlem14  39885  pclfinclN  39951  ismrc  42696  fzsplit1nn0  42749  pell1234qrmulcl  42850  pell14qrmulcl  42858  onsucf1olem  43266  iunrelexp0  43698  bi23impib  44483  bi13impib  44484  trelded  44562  suctrALT  44822  suctrALTcf  44918  suctrALTcfVD  44919  stoweidlem17  46022  zm1nn  47307  bgoldbtbndlem4  47813  bgoldbtbnd  47814  tgblthelfgott  47820  vopnbgrelself  47859  clnbgr3stgrgrlic  48015  clcllaw  48183  ztprmneprm  48339  lcoel0  48421  linindslinci  48441  fv2arycl  48641