Theorem 3expib 1123

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expib	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1120	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 410	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:  3anidm12  1422  mob  3677  dfss2  3921  eqbrrdva  5826  f1oiso2  7308  frxp  8078  onfununi  8283  smoel2  8305  smoiso2  8311  3ecoptocl  8758  ssfi  9109  f1domfi  9117  rex2dom  9165  fodomfib  9241  dffi2  9338  elfiun  9345  dif1card  9932  infxpenlem  9935  cfeq0  10178  cfsuc  10179  cfflb  10181  cfslb2n  10190  cofsmo  10191  domtriomlem  10364  axdc3lem4  10375  axdc4lem  10377  ttukey2g  10438  tskxpss  10695  grudomon  10740  elnpi  10911  dedekind  11308  nn0n0n1ge2b  12482  fzind  12602  suprzcl2  12863  icoshft  13401  fzen  13469  hashgt23el  14359  hashfundm  14377  hashbclem  14387  seqcoll  14399  relexpsucl  14966  relexpsucr  14967  relexpfld  14984  shftuz  15004  mulgcd  16487  algcvga  16518  lcmneg  16542  ressbas  17175  resseqnbas  17181  ressress  17186  psss  18515  tsrlemax  18521  isnmgm  18581  gsummgmpropd  18618  issgrpd  18667  iscmnd  19735  ring1ne0  20246  unitmulclb  20329  isdrngd  20710  isdrngdOLD  20712  abvn0b  20781  issrngd  20800  rmodislmodlem  20892  rmodislmod  20893  isphld  21621  mpfaddcl  22080  mpfmulcl  22081  pf1addcl  22309  pf1mulcl  22310  fitop  22856  hausnei2  23309  ordtt1  23335  locfincmp  23482  basqtop  23667  filfi  23815  fgcl  23834  neifil  23836  filuni  23841  cnextcn  24023  prdsmet  24326  blssps  24380  blss  24381  metcnp3  24496  hlhil  25411  volsup2  25574  sincosq1sgn  26475  sincosq2sgn  26476  sincosq3sgn  26477  sincosq4sgn  26478  sinq12ge0  26485  bcmono  27256  n0cutlt  28367  bdayfin  28495  iswlkg  29699  usgrwwlks2on  30043  umgrwwlks2on  30044  clwlkclwwlkfo  30096  3cyclfrgrrn1  30372  grpodivf  30625  ipf  30800  shintcli  31416  spanuni  31631  adjadj  32023  unopadj2  32025  hmopadj  32026  hmopbdoptHIL  32075  resvsca  33424  resvlem  33425  submateq  33986  esumcocn  34257  bnj1379  35005  bnj571  35081  bnj594  35087  bnj580  35088  bnj600  35094  bnj1189  35184  bnj1321  35202  bnj1384  35207  f1resrcmplf1dlem  35261  trssfir1om  35286  fineqvinfep  35300  trssfir1omregs  35311  cplgredgex  35334  cusgr3cyclex  35349  loop1cycl  35350  umgr2cycllem  35353  umgr2cycl  35354  acycgr2v  35363  cusgracyclt3v  35369  climuzcnv  35884  fness  36562  cgsex2gd  37386  bj-idreseq  37411  bj-imdiridlem  37434  neificl  37998  metf1o  38000  isismty  38046  ismtybndlem  38051  ablo4pnp  38125  divrngcl  38202  keridl  38277  prnc  38312  lsmsatcv  39380  llncvrlpln2  39927  lplncvrlvol2  39985  linepsubN  40122  pmapsub  40138  dalawlem10  40250  dalawlem13  40253  dalawlem14  40254  dalaw  40256  diaf11N  41419  dibf11N  41531  ismrcd1  43049  ismrcd2  43050  mzpincl  43085  mzpadd  43089  mzpmul  43090  pellfundge  43233  imasgim  43451  sqrtcval  43991  stoweidlem2  46354  stoweidlem17  46369  imaelsetpreimafv  47749  opnneir  49260  i0oii  49273  io1ii  49274