Theorem 3impib 1114

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

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

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 396  df-3an 1087

This theorem is referenced by:  3impia  1115  mob  3647  eqreu  3659  dedth3h  4516  prproe  4834  rbropap  5469  breldmg  5807  ssimaexg  6836  funopdmsn  7004  fpr3g  8072  wfr3g  8109  dfsmo2  8149  omwordri  8365  3ecoptocl  8556  frr3g  9445  cfslb  9953  cofsmo  9956  cfsmolem  9957  coftr  9960  domtriomlem  10129  zorn2lem7  10189  ttukey2g  10203  gchi  10311  tskxpss  10459  tskord  10467  infm3  11864  uzind  12342  fzind  12348  fnn0ind  12349  xltnegi  12879  axdc4uz  13632  facwordi  13931  swrdnd2  14296  cshwidxmod  14444  relexpsucl  14670  relexpsucr  14671  relexprelg  14677  relexpaddnn  14690  caubnd  14998  mulgcd  16184  lcmfdvds  16275  lcmfdvdsb  16276  coprmdvds1  16285  pcfac  16528  ramz  16654  imasleval  17169  cictr  17434  initoeu2lem1  17645  drsdir  17935  psasym  18209  pstr  18210  tsrlin  18218  dirge  18236  mgmcl  18244  mhmlin  18352  mhmmulg  18659  issubg2  18685  nsgbi  18700  cygablOLD  19407  gsumcom2  19491  srgmulgass  19682  dvdsrtr  19809  drnginvrcl  19923  drnginvrn0  19924  drnginvrl  19925  drnginvrr  19926  isdrngd  19931  issubrg2  19959  abvmul  20004  abvtri  20005  lmhmlin  20212  domnmuln0  20482  ipcj  20751  cssincl  20805  obsip  20838  decpmatmulsumfsupp  21830  mp2pm2mplem4  21866  pm2mpghm  21873  pm2mpmhmlem1  21875  inopn  21956  basis1  22008  iscldtop  22154  2ndcdisj  22515  cnmpt2t  22732  cnmpt22  22733  cnmptcom  22737  fbasssin  22895  ptcmplem3  23113  xmeteq0  23399  prdsxmslem2  23591  nmvs  23746  nmolb  23787  volfiniun  24616  sincosq1sgn  25560  sincosq2sgn  25561  sincosq3sgn  25562  sincosq4sgn  25563  ewlkle  27875  wwlksnext  28159  umgr2adedgwlklem  28210  elwwlks2ons3im  28220  umgrwwlks2on  28223  conngrv2edg  28460  frgrwopregasn  28581  frgrwopregbsn  28582  frgrwopreglem5  28586  frgrwopreglem5ALT  28587  frgr2wwlkeu  28592  ablocom  28811  nmcvcn  28958  ipassi  29104  htth  29181  shaddcl  29480  shmulcl  29481  shsubcl  29483  chlimi  29497  pjspansn  29840  cnopc  30176  cnfnc  30193  adj1  30196  lnfnmul  30311  atord  30651  atcvat2  30652  cdj3i  30704  nexple  31877  signstfvc  32453  bnj910  32828  bnj1154  32879  umgr2cycllem  33002  pconncn  33086  mrsubccat  33380  shftvalg  33603  ttrclselem2  33712  linethru  34382  sin2h  35694  cos2h  35695  tan2h  35696  dvasin  35788  areacirclem1  35792  riotasv  36900  lsmsatcv  36951  omllaw  37184  2llnjN  37508  dalawlem10  37821  dalawlem13  37824  dalawlem14  37825  pclfinclN  37891  ismrc  40439  fzsplit1nn0  40492  pell1234qrmulcl  40593  pell14qrmulcl  40601  iunrelexp0  41199  bi23impib  41994  bi13impib  41995  trelded  42074  suctrALT  42335  suctrALTcf  42431  suctrALTcfVD  42432  stoweidlem17  43448  zm1nn  44682  bgoldbtbndlem4  45148  bgoldbtbnd  45149  tgblthelfgott  45155  mgmhmlin  45228  issubmgm2  45232  clcllaw  45273  rnghmmul  45346  ztprmneprm  45571  lcoel0  45657  linindslinci  45677  fv2arycl  45882