Theorem 3impia 1114

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 452	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1113	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  mopick2  2625  ceqsalt  3494  3gencl  3506  vtoclgft  3530  vtoclegft  3568  rspc6v  3626  mob2  3707  moi  3710  reupick3  4319  disjne  4456  elpr2elpr  4871  disji2  5131  disji  5132  tz7.2  5662  sofld  6193  ordintdif  6421  funopg  6588  fvun1  6988  fvopab6  7038  fveqressseq  7088  fvcofneq  7102  fprg  7164  2f1fvneq  7270  isores3  7342  ovmpt4g  7568  ovmpos  7569  ov2gf  7570  ofrval  7697  sorpssuni  7738  sorpssint  7739  poxp  8133  poseq  8163  suppss2  8206  frrlem12  8303  smoel  8381  smoord  8386  smogt  8388  oaass  8582  oewordi  8612  oeoalem  8617  oeoelem  8619  nnawordi  8642  nnaass  8643  naddssim  8706  qsel  8815  xpdom3  9095  onsdominel  9151  mapdom3  9174  sdomdomtrfi  9229  domsdomtrfi  9230  php  9235  onomeneq  9253  fisseneq  9282  cantnflem1  9714  ttrclss  9745  cfslbn  10292  cfsmolem  10295  cfcoflem  10297  infpssrlem4  10331  fin23lem7  10341  fin23lem25  10349  isf34lem7  10404  hsmexlem2  10452  axcc3  10463  axdc4lem  10480  tskss  10783  gruss  10821  gruurn  10823  gruiun  10824  gruel  10828  gruen  10837  grudomon  10842  grothac  10855  axpre-sup  11194  axsup  11321  addn0nid  11666  letrp1  12091  p1le  12092  lemul1a  12101  infrelb  12232  zextle  12668  zextlt  12669  btwnnz  12671  gtndiv  12672  uzind2  12688  fzind  12693  eluzsubOLD  12891  zsupss  12954  xrltne  13177  lemaxle  13209  qbtwnre  13213  qbtwnxr  13214  xlemul1a  13302  icogelb  13410  iccleub  13414  iccsplit  13497  uzsubsubfz  13558  elfz0fzfz0  13641  difelfznle  13650  fvffz0  13654  elfzo0le  13711  fzonmapblen  13713  fzofzim  13714  ceile  13850  modadd1  13909  muladdmodid  13912  modmul1  13925  modirr  13943  fsuppmapnn0fiub0  13994  expcl2lem  14074  expclzlem  14084  expnegz  14097  leexp2r  14174  bcval4  14302  bccmpl  14304  hashbnd  14331  hashunsnggt  14389  hashgt23el  14419  hashfundm  14437  elovmpowrd  14544  ccatval2  14564  ccatrcl1  14580  wrdl1s1  14600  ccat2s1fvw  14624  swrdsb0eq  14649  swrdccatin1  14711  pfxccatpfx2  14723  repswswrd  14770  cshwcsh2id  14815  absexpz  15288  climbdd  15654  iseraltlem2  15665  binomfallfac  16021  dvdsle  16290  divalgb  16384  ndvdssub  16389  dvdsgcd  16523  dfgcd2  16525  rplpwr  16536  lcmgcdlem  16580  lcmfunsn  16618  coprmdvds1  16626  qredeq  16631  2mulprm  16667  prmdvdsexpr  16691  nnnn0modprm0  16778  prm23ge5  16787  pcexp  16831  difsqpwdvds  16859  prmpwdvds  16876  ramcl  17001  cshwshashlem3  17070  cshwrepswhash1  17075  elrestr  17413  mreintcl  17578  mremre  17587  mrieqv2d  17622  initoeu2lem1  18006  funcestrcsetclem9  18142  funcsetcestrclem9  18157  prstr  18295  drsdirfi  18300  latnlej  18451  latnlej2  18454  acsdrsel  18538  acsdrscl  18541  mrelatglb  18555  mrelatlub  18557  isnmgm  18607  grpasscan1  18966  grpinvnz  18974  mulgneg2  19071  gsmsymgrfix  19395  f1omvdco2  19415  symggen  19437  odcl2  19532  odhash3  19543  lsmss1  19632  lsmss2  19634  efgred  19715  efgcpbl  19723  ablfacrp  20035  ablfac1eu  20042  ablfaclem3  20056  dvdsrmul1  20320  dvdsunit  20330  irredmul  20380  c0snmgmhm  20413  lmodlema  20760  psgnodpmr  21539  phlssphl  21608  lindsss  21775  lindfmm  21778  ply1scln0  22236  dmatelnd  22442  mdetdiaglem  22544  mdet0  22552  mdetunilem7  22564  slesolinv  22626  cramerimplem3  22631  cpmatpmat  22656  m2cpminvid2lem  22700  chfacfscmul0  22804  chfacfpmmul0  22808  riinopn  22854  clsndisj  23023  cnpf2  23198  hausnei2  23301  cmpcov  23337  cmpfii  23357  unconn  23377  t1connperf  23384  nrmr0reg  23697  fbfinnfr  23789  filuni  23833  alexsubALT  23999  tmdgsum  24043  cuspcvg  24250  mopni  24445  isngp4  24565  metdsre  24813  iimulcl  24904  phtpc01  24966  clmmulg  25072  cfilucfil4  25293  bcthlem5  25300  bcth  25301  bcth3  25303  itg1le  25687  itg2le  25713  bddmulibl  25812  bddiblnc  25815  dvnres  25905  cpnord  25909  dvnfre  25928  deg1ge  26078  dgr1term  26239  aaliou3lem2  26323  sincosq1lem  26477  cxpge0  26662  cxpmul2  26668  logrec  26740  logbgcd1irr  26771  sqfpc  27114  bcmono  27255  gausslemma2dlem1a  27343  gausslemma2dlem2  27345  gausslemma2dlem4  27347  2lgsoddprmlem3  27392  pntrmax  27542  qabvexp  27604  ostth2lem2  27612  nosepon  27644  nolesgn2o  27650  nogesgn1o  27652  nosepnelem  27658  nosepne  27659  nosepdmlem  27662  nosepdm  27663  nodenselem8  27670  noresle  27676  noetasuplem4  27715  noetainflem4  27719  scutbdaylt  27797  addsuniflem  27964  ssltmul1  28097  precsexlem6  28160  precsexlem7  28161  precsexlem11  28165  sltonold  28203  ax5seglem4  28815  axeuclidlem  28845  uhgredgrnv  29015  usgredg4  29102  nbuhgr2vtx1edgblem  29236  vtxduhgr0e  29364  vtxduhgr0nedg  29378  rusgrpropnb  29469  uspgr2wlkeqi  29534  redwlklem  29557  lfgrwlkprop  29573  2pthnloop  29617  spthonepeq  29638  pthdlem2lem  29653  crctcshwlkn0lem3  29695  crctcshwlkn0lem5  29697  crctcshwlkn0lem7  29699  crctcshwlkn0  29704  wlkiswwlks1  29750  wlkiswwlks2  29758  wlkiswwlksupgr2  29760  wwlksnext  29776  wwlksnextproplem2  29793  wspthsnonn0vne  29800  2pthon3v  29826  rusgrnumwwlk  29858  erclwwlkeqlen  29901  erclwwlksym  29903  erclwwlktr  29904  erclwwlkneqlen  29950  erclwwlknsym  29952  erclwwlkntr  29953  uhgr3cyclex  30064  upgreupthseg  30091  eupth2lem3lem4  30113  eucrctshift  30125  4cycl2vnunb  30172  nvs  30545  nvtri  30552  nmlno0  30677  nmlnoubi  30678  ubth  30755  hlipgt0  30796  ocnel  31180  elspansn2  31449  elspansn3  31454  normcan  31458  pjoml2  31493  lecm  31499  osum  31527  nmbdfnlb  31932  leopmul  32016  hstpyth  32111  cvnbtwn  32168  ssmd1  32193  ssmd2  32194  ssdmd1  32195  ssdmd2  32196  cvmd  32218  cvdmd  32219  superpos  32236  disji2f  32446  disjif  32447  disjif2  32450  preiman0  32571  padct  32583  ffs2  32592  bcm1n  32645  s2f1  32755  omndadd  32876  ogrpaddlt  32887  archiabl  32998  slmdlema  33002  lbslsat  33445  eulerpartlemb  34119  sgn3da  34292  fisshasheq  34855  cvmsdisj  35011  cvmlift2lem12  35055  satfrel  35108  satfrnmapom  35111  fmlasuc  35127  satffun  35150  satef  35157  sategoelfv  35161  lineintmo  35884  nn0prpwlem  35937  nn0prpw  35938  neibastop2lem  35975  lindsadd  37217  areacirc  37317  incsequz  37352  mettrifi  37361  ismtybnd  37411  heiborlem1  37415  rngoisocnv  37585  risci  37591  eqvrelqsel  38218  lfl1  38672  lkrlsp2  38705  omlfh3N  38861  cvrnbtwn  38873  cvrnbtwn2  38877  cvrnbtwn4  38881  cvlexch3  38934  cvlexch4N  38935  cvlatexchb1  38936  2llnne2N  39011  atcvrj0  39031  cvrat2  39032  ps-1  39080  3atlem5  39090  islln2a  39120  lplnriaN  39153  lplnribN  39154  llncvrlpln2  39160  lplncvrlvol2  39218  psubatN  39358  pmapglb2N  39374  pmapglb2xN  39375  2llnma1b  39389  paddasslem17  39439  pmod2iN  39452  pmodl42N  39454  hlmod1i  39459  atmod1i1  39460  atmod1i2  39462  llnmod1i2  39463  pclcmpatN  39504  osumcllem8N  39566  pexmidlem3N  39575  pl42lem4N  39585  4atexlem7  39678  ltrnnid  39739  cdlemc4  39797  cdleme32a  40044  cdlemeg46gfre  40135  cdlemf2  40165  cdlemg4c  40215  trlcoat  40326  tendovalco  40368  tendoeq2  40377  cdlemk36  40516  diael  40646  diatrl  40647  dicelval1stN  40791  dicelval2nd  40792  dihlspsnat  40936  dochkr1  41081  lcfrlem9  41153  mapdh8e  41387  hdmapval0  41436  hgmapval0  41495  nnadddir  41980  nn0rppwr  42028  nn0expgcd  42030  dvdsexpnn0  42036  incssnn0  42273  pell14qrexpcl  42429  pell14qrgap  42437  congadd  42529  acongsym  42539  acongtr  42541  dvdsacongtr  42547  jm2.19lem3  42554  jm2.19lem4  42555  jm2.26lem3  42564  onexlimgt  42813  nadd2rabex  42957  ismnushort  43880  bi13impia  44069  3impcombi  44398  ioogtlb  45018  iocgtlb  45025  iocleub  45026  icoltub  45031  iooltub  45033  limclner  45177  limsupre3lem  45258  climuzlem  45269  fsupdm  46368  finfdm  46372  elfzelfzlble  46839  subsubelfzo0  46844  iccpartigtl  46900  sqrtpwpw2p  47015  fmtnoprmfac1lem  47041  fmtno4prmfac  47049  evenltle  47194  even3prm2  47196  wtgoldbnnsum4prm  47279  bgoldbnnsum3prm  47281  bgoldbtbndlem1  47282  bgoldbtbndlem3  47284  bgoldbtbndlem4  47285  bgoldbtbnd  47286  upgrwlkupwlk  47388  funcringcsetcALTV2lem9  47546  funcringcsetclem9ALTV  47569  lincscmcl  47686  lindslinindimp2lem4  47715  lincresunit2  47732  lincresunit3  47735  elfzolborelfzop1  47773  m1modmmod  47780  rege1logbzge0  47818  fllog2  47827  dignn0ldlem  47861  rrx2pnecoorneor  47974  rrx2plord2  47981  rrx2linest  48001  ipolub  48185  ipoglb  48188